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 (len p) + (len q) by Def4;
then A1: k < (len p) + (len q) by NAT_1:45;

now

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:16;
then n in len q by NAT_1:45;
hence ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A2; :: thesis: verum

end;

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