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

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