let p, q be FinSequence; ( p <> {} & q <> {} implies (len (p $^ q)) + 1 = (len p) + (len q) )
assume
( p <> {} & q <> {} )
; (len (p $^ q)) + 1 = (len p) + (len q)
then consider i being Nat, r being FinSequence such that
A1:
( len p = i + 1 & r = p | (Seg i) & p $^ q = r ^ q )
by Def1;
A2:
i <= len p
by A1, NAT_1:11;
thus (len (p $^ q)) + 1 =
((len r) + (len q)) + 1
by A1, FINSEQ_1:22
.=
(i + (len q)) + 1
by A1, A2, FINSEQ_1:17
.=
(len p) + (len q)
by A1
; verum