let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n, k, l 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 m, n, k, l being Nat st m <= n & k <= l holds
(A |^ m,n) ^^ (A |^ k,l) = A |^ (m + k),(n + l)
let m, n, k, l 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

let x be set ; :: 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:18;
then A |^ (mn + kl) c= (A |^ m,n) ^^ (A |^ k,l) by FLANG_1:34;
hence x in (A |^ m,n) ^^ (A |^ k,l) by A4, A5; :: thesis: verum

end;

now

let x be set ; :: 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:9;
( a ^ b in A |^ (mn + kl) & m + k <= mn + kl ) by A13, A15, A10, A12, FLANG_1:41, XREAL_1:9;
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