Theorem·T30
Concatenation of a sequence of sequences exists and is unique
The recursive concatenation rule genuinely determines exactly one sequence, for any finite number of pieces.
In words
For any finite length n and any sequence t of sequences from A with exactly n entries, the concatenation of all of t, computed by the recursive rule of joining one more piece at a time, genuinely exists and is genuinely unique.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1By strong induction on : we show that for every and every with , there is a unique satisfying the two characterizing clauses of D080 (the second vacuous when , since then no has , (P3)).
- 2Base : the only with is . Take : the first clause holds directly, the second vacuously. Uniqueness: the first clause forces .
- 3Step: assume the claim for : for every length- sequence of sequences , exists uniquely. Let with , and let be its restriction to ( since ), a length- sequence of sequences. By the induction hypothesis exists uniquely; define using concatenation ( , valid by T29). This satisfies the second clause by construction, and the first vacuously ( , (P3)).
- 4Uniqueness at : any satisfying the clauses for this must, by the (non-vacuous) second clause, equal , the very expression defining , since is already pinned down uniquely by the induction hypothesis. So .
- 5T08 concludes: existence and uniqueness hold for every and every of that length.
∎
Remarks
Confirms the notation
is well posed. The proof is the exact strong-induction shape already used for the Euclidean algorithm and Bezout's identity: prove the base case directly, and reduce the step case to an already-settled smaller instance via the induction hypothesis.