let E be set ; :: thesis: for A, B, C 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, B, C 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 that

A1: A c= C |^.. m and

A2: B c= C |^.. n ; :: thesis: A ^^ B c= C |^.. (m + n)

thus for x being object st x in A ^^ B holds

x in C |^.. (m + n) :: according to TARSKI:def 3 :: thesis: verum

for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds

A ^^ B c= C |^.. (m + n)

let A, B, C 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 that

A1: A c= C |^.. m and

A2: B c= C |^.. n ; :: thesis: A ^^ B c= C |^.. (m + n)

thus for x being object st x in A ^^ B holds

x in C |^.. (m + n) :: according to TARSKI:def 3 :: thesis: verum

proof

let x be object ; :: 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

A3: a in A and

A4: b in B and

A5: x = a ^ b by FLANG_1:def 1;

a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, A3, A4, FLANG_1:def 1;

hence x in C |^.. (m + n) by A5, Th18; :: thesis: verum

end;assume x in A ^^ B ; :: thesis: x in C |^.. (m + n)

then consider a, b being Element of E ^omega such that

A3: a in A and

A4: b in B and

A5: x = a ^ b by FLANG_1:def 1;

a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, A3, A4, FLANG_1:def 1;

hence x in C |^.. (m + n) by A5, Th18; :: thesis: verum