let E be set ; :: thesis: for A, B, C being Subset of (E ^omega)
for k, l, m, n 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, B, C be Subset of (E ^omega); :: thesis: for k, l, m, n 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 k, l, m, n 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 that
A1: ( m <= n & k <= l ) and
A2: ( 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 object ; :: 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
A3: ( a in A & b in B ) and
A4: x = a ^ b by FLANG_1:def 1;
a ^ b in (C |^ (m,n)) ^^ (C |^ (k,l)) by A2, A3, FLANG_1:def 1;
hence x in C |^ ((m + k),(n + l)) by A1, A4, Th37; :: thesis: verum

end;