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,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
A3: ( a in A |^ m,n & b in A |^ k,l & x = a ^ b ) by FLANG_1:def 1;
consider mn being Nat such that
A4: ( m <= mn & mn <= n & a in A |^ mn ) by A3, Th19;
consider kl being Nat such that
A5: ( k <= kl & kl <= l & b in A |^ kl ) by A3, Th19;
A6: a ^ b in A |^ (mn + kl) by A4, A5, FLANG_1:41;
A7: m + k <= mn + kl by A4, A5, XREAL_1:9;
mn + kl <= n + l by A4, A5, XREAL_1:9;
hence x in A |^ (m + k),(n + l) by A3, A6, A7, Th19; :: thesis: verum

end;

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
A8: ( m + k <= i & i <= n + l & x in A |^ i ) by Th19;
consider mn, kl being Nat such that
A9: ( mn + kl = i & m <= mn & mn <= n & k <= kl & kl <= l ) by A1, A8, Th2;
A10: A |^ mn c= A |^ m,n by A9, Th20;
A |^ kl c= A |^ k,l by A9, Th20;
then (A |^ mn) ^^ (A |^ kl) c= (A |^ m,n) ^^ (A |^ k,l) by A10, 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 A8, A9; :: thesis: verum

end;

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