let E be set ; :: thesis: for A, C, B being Subset of (E ^omega )
for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)
let A, C, B be Subset of (E ^omega ); :: thesis: for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)
let m, n be Nat; :: thesis: ( A c= C |^.. m & B c= C |^.. n implies A ^^ B c= C |^.. (m + n) )
assume A1: ( A c= C |^.. m & B c= C |^.. n ) ; :: thesis: A ^^ B c= C |^.. (m + n)
thus for x being set st x in A ^^ B holds
x in C |^.. (m + n) :: according to TARSKI:def 3 :: thesis: verum

proof

let x be set ; :: thesis: ( x in A ^^ B implies x in C |^.. (m + n) )
assume x in A ^^ B ; :: thesis: x in C |^.. (m + n)
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) ^^ (C |^.. n) by A1, A2, FLANG_1:def 1;
hence x in C |^.. (m + n) by A2, Th18; :: thesis: verum

end;