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 ) )
A1: k in NAT by ORDINAL1:def 13;
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 Seg (len (p ^ q)) by Def3;
then A2: k in Seg ((len p) + (len q)) by Th35;
then A3: ( 1 <= k & k <= (len p) + (len q) ) by Th3;

A4: now

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 A1, 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

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;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
(len p) + (1 + n) <= (len p) + (len q) by A2, A5, Th3;
then A6: 1 + n <= len q by XREAL_1:8;
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