theorem :: FLANG_2:58

for E being set
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))