Theorem·T29
Concatenation produces a finite sequence of the expected length
Concatenating two finite sequences gives a finite sequence whose length is the sum of the lengths and which agrees with each piece in its place.
For
a set and
with
, the concatenation
(D075) is a finite sequence:
,
and, writing
:
In words
For finite sequences f, g from A, with f of length m: the length of f‸g is m plus g's length, its entries below m are f's, and its entries from m on are g's, shifted by m.
Never needed: F05 · F10 · F13 · A02 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1
- 2Domain. (each contributes exactly one pair, with first coordinate ). So the last equality by L60.
- 3Single-valued. Let . If : assigns the value ; the second part assigns a value at only if for some , but then (L17 (i)), contradicting (i.e. , D029). So only assigns a value at . If for some (the remaining case, by the domain computed above): means assigns no value at (since , so by the same reasoning); and among the pairs for , only gives first coordinate , since forces by cancellation. So exactly one value is assigned at in every case: is single-valued, hence a function .
- 4Values. For : , so by single-valuedness . For : by construction, so .
- 5So is a function with domain and values in : (D074), of length , agreeing with below and with (shifted by ) beyond.
∎
Remarks
The basic algebraic fact about concatenation. Associativity,
, and the length-
empty sequence acting as an identity, are not separately verified here; concatenation is the first piece of machinery needed to eventually build strings over a formal alphabet, and then terms and formulas, toward the recursive definitions used in a formal treatment of first-order logic.