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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^^ B or x in C |^ (m + k),(n + l) )
assume x in A ^^ B ; :: thesis: x in C |^ (m + k),(n + l)
then consider a, b being Element of E ^omega such that
A2: ( a in A & b in B & x = a ^ b ) by FLANG_1:def 1;
a ^ b in (C |^ m,n) ^^ (C |^ k,l) by A1, A2, FLANG_1:def 1;
hence x in C |^ (m + k),(n + l) by A1, A2, Th37; :: thesis: verum

end;