let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, l, m, n being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
let A be Subset of (E ^omega); :: thesis: for k, l, m, n being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
let k, l, m, n be Nat; :: thesis: ( m <= n & k <= l implies (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l)) )
assume A1: ( m <= n & k <= l ) ; :: thesis: (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))

A2: now :: thesis: for x being object st x in A |^ ((m + k),(n + l)) holds
x in (A |^ (m,n)) ^^ (A |^ (k,l))

let x be object ; :: thesis: ( x in A |^ ((m + k),(n + l)) implies x in (A |^ (m,n)) ^^ (A |^ (k,l)) )
assume x in A |^ ((m + k),(n + l)) ; :: thesis: x in (A |^ (m,n)) ^^ (A |^ (k,l))
then consider i being Nat such that
A3: ( m + k <= i & i <= n + l ) and
A4: x in A |^ i by Th19;
consider mn, kl being Nat such that
A5: mn + kl = i and
A6: ( m <= mn & mn <= n & k <= kl & kl <= l ) by A1, A3, Th2;
( A |^ mn c= A |^ (m,n) & A |^ kl c= A |^ (k,l) ) by A6, Th20;
then (A |^ mn) ^^ (A |^ kl) c= (A |^ (m,n)) ^^ (A |^ (k,l)) by FLANG_1:17;
then A |^ (mn + kl) c= (A |^ (m,n)) ^^ (A |^ (k,l)) by FLANG_1:33;
hence x in (A |^ (m,n)) ^^ (A |^ (k,l)) by A4, A5; :: thesis: verum

end;

now :: thesis: for x being object st x in (A |^ (m,n)) ^^ (A |^ (k,l)) holds
x in A |^ ((m + k),(n + l))

let x be object ; :: thesis: ( x in (A |^ (m,n)) ^^ (A |^ (k,l)) implies x in A |^ ((m + k),(n + l)) )
assume x in (A |^ (m,n)) ^^ (A |^ (k,l)) ; :: thesis: x in A |^ ((m + k),(n + l))
then consider a, b being Element of E ^omega such that
A7: a in A |^ (m,n) and
A8: b in A |^ (k,l) and
A9: x = a ^ b by FLANG_1:def 1;
consider kl being Nat such that
A10: k <= kl and
A11: kl <= l and
A12: b in A |^ kl by A8, Th19;
consider mn being Nat such that
A13: m <= mn and
A14: mn <= n and
A15: a in A |^ mn by A7, Th19;
A16: mn + kl <= n + l by A14, A11, XREAL_1:7;
( a ^ b in A |^ (mn + kl) & m + k <= mn + kl ) by A13, A15, A10, A12, FLANG_1:40, XREAL_1:7;
hence x in A |^ ((m + k),(n + l)) by A9, A16, Th19; :: thesis: verum

end;

hence (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l)) by A2, TARSKI:2; :: thesis: verum