let k be Nat; :: thesis: for p, q being XFinSequence 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 p, q be XFinSequence; :: 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 k in Segm ((len p) + (len q)) by Def3;
then A1: k < (len p) + (len q) by NAT_1:44;

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

assume len p <= 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
A2: k = (len p) + n by NAT_1:10;
(n + (len p)) - (len p) < ((len q) + (len p)) - (len p) by A1, A2, XREAL_1:14;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A2, Lm1; :: thesis: verum

end;

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