let p, q be FinSequence; :: thesis: for k being Nat holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
let k be Nat; :: thesis: ( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
assume k in dom (p ^ q) ; :: thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then A1: k in Seg (len (p ^ q)) by Def3;
then A2: k in Seg ((len p) + (len q)) by Th22;
A3: ( k in NAT & 1 <= k ) by A1, Th1;

A4: now :: thesis: ( (len p) + 1 <= k or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )

assume not (len p) + 1 <= k ; :: thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then k <= len p by NAT_1:8;
then k in Seg (len p) by A3;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by Def3; :: thesis: verum

end;

now :: thesis: ( not (len p) + 1 <= k or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )

assume (len p) + 1 <= k ; :: thesis: ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )
then consider n being Nat such that
A5: k = ((len p) + 1) + n by NAT_1:10;
(len p) + (1 + n) <= (len p) + (len q) by A2, A5, Th1;
then A6: 1 + n <= len q by XREAL_1:6;
1 <= 1 + n by NAT_1:11;
then 1 + n in Seg (len q) by A6;
then A7: 1 + n in dom q by Def3;
k = (len p) + (1 + n) by A5;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A7; :: thesis: verum

end;

hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A4; :: thesis: verum