let p, q, r be FinSequence; :: thesis: ( len r = (len p) + (len q) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ) implies r = p ^ q )
assume len r = (len p) + (len q) ; :: thesis: ( ex k being Nat st
( k in dom p & not r . k = p . k ) or ex k being Nat st
( k in dom q & not r . ((len p) + k) = q . k ) or r = p ^ q )
then A1: dom r = Seg ((len p) + (len q)) by FINSEQ_1:def 3;
assume that
A2: for k being Nat st k in dom p holds
r . k = p . k and
A3: for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ; :: thesis: r = p ^ q
A4: for k being Nat st k in dom q holds
r . ((len p) + k) = q . k by A3;
for k being Nat st k in dom p holds
r . k = p . k by A2;
hence r = p ^ q by A1, A4, FINSEQ_1:def 7; :: thesis: verum