defpred S₂[ set , set ] means ( ( for k being Nat st k = $1 & 1 <= k & k <= len p holds
$2 = p . k ) & ( for k being Nat st k = $1 & (len p) + 1 <= k & k <= (len p) + (len q) holds
$2 = q . (k - (len p)) ) );
A1: for x being set st x in Seg ((len p) + (len q)) holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in Seg ((len p) + (len q)) implies ex y being set st S₂[x,y] )
assume x in Seg ((len p) + (len q)) ; :: thesis: ex y being set st S₂[x,y]
then reconsider m = x as Element of NAT ;

A2: now :: thesis: ( (len p) + 1 <= m implies ex y being set st S₂[x,y] )

assume A3: (len p) + 1 <= m ; :: thesis: ex y being set st S₂[x,y]
set y = q . (m - (len p));
A4: for k being Nat st k = x & 1 <= k & k <= len p holds
q . (m - (len p)) = p . k

proof

let k be Nat; :: thesis: ( k = x & 1 <= k & k <= len p implies q . (m - (len p)) = p . k )
assume that
A5: k = x and
1 <= k and
A6: k <= len p ; :: thesis: q . (m - (len p)) = p . k
m + ((len p) + 1) <= m + (len p) by A3, A5, A6, XREAL_1:7;
then (m + (len p)) + 1 <= (m + (len p)) + 0 ;
hence q . (m - (len p)) = p . k by XREAL_1:6; :: thesis: verum

end;

for k being Nat st k = x & (len p) + 1 <= k & k <= (len p) + (len q) holds
q . (m - (len p)) = q . (k - (len p)) ;
hence ex y being set st S₂[x,y] by A4; :: thesis: verum

end;

now :: thesis: ( not (len p) + 1 <= m implies ex y being set st S₂[x,y] )

assume A7: not (len p) + 1 <= m ; :: thesis: ex y being set st S₂[x,y]
set y = p . m;
( ( for k being Nat st k = x & 1 <= k & k <= len p holds
p . m = p . k ) & ( for k being Nat st k = x & (len p) + 1 <= k & k <= (len p) + (len q) holds
p . m = q . (k - (len p)) ) ) by A7;
hence ex y being set st S₂[x,y] ; :: thesis: verum

end;

hence ex y being set st S₂[x,y] by A2; :: thesis: verum

end;

consider f being Function such that
A8: ( dom f = Seg ((len p) + (len q)) & ( for x being set st x in Seg ((len p) + (len q)) holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A1);
A9: for k being Nat st k in dom p holds
f . k = p . k

proof

let k be Nat; :: thesis: ( k in dom p implies f . k = p . k )
assume k in dom p ; :: thesis: f . k = p . k
then A10: k in Seg (len p) by Def3;
then A11: ( 1 <= k & k <= len p ) by Th1;
len p <= (len p) + (len q) by NAT_1:11;
then Seg (len p) c= Seg ((len p) + (len q)) by Th5;
hence f . k = p . k by A8, A10, A11; :: thesis: verum

end;

A12: for n being Nat st n in dom q holds
f . ((len p) + n) = q . n

proof

let n be Nat; :: thesis: ( n in dom q implies f . ((len p) + n) = q . n )
assume n in dom q ; :: thesis: f . ((len p) + n) = q . n
then A13: n in Seg (len q) by Def3;
then A14: 1 <= n by Th1;
A15: n <= len q by A13, Th1;
A16: (len p) + 1 <= (len p) + n by A14, XREAL_1:7;
A17: (len p) + n <= (len p) + (len q) by A15, XREAL_1:7;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
(len p) + n <= ((len p) + n) + (len p) by NAT_1:11;
then (len p) + 1 <= ((len p) + n) + (len p) by A16, XXREAL_0:2;
then 1 <= (len p) + n by XREAL_1:6;
then (len p) + n in Seg ((len p) + (len q)) by A17;
then f . ((len p) + n) = q . ((n + (len p)) - (len p)) by A8, A16, A17;
hence f . ((len p) + n) = q . n ; :: thesis: verum

end;

reconsider r = f as FinSequence by A8, Def2;
take r ; :: thesis: ( dom r = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ) )
thus ( dom r = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
r . k = p . k ) & ( for k being Nat st k in dom q holds
r . ((len p) + k) = q . k ) ) by A8, A9, A12; :: thesis: verum