let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n, k, l being Nat holds (A |^ m,n) |^ k,l c= A |^ (m * k),(n * l)
let A be Subset of (E ^omega ); :: thesis: for m, n, k, l being Nat holds (A |^ m,n) |^ k,l c= A |^ (m * k),(n * l)
let m, n, k, l be Nat; :: thesis: (A |^ m,n) |^ k,l c= A |^ (m * k),(n * l)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ m,n) |^ k,l or x in A |^ (m * k),(n * l) )
assume x in (A |^ m,n) |^ k,l ; :: thesis: x in A |^ (m * k),(n * l)
then consider kl being Nat such that
A1: ( k <= kl & kl <= l ) and
A2: x in (A |^ m,n) |^ kl by Th19;
( m * k <= m * kl & n * kl <= n * l ) by A1, NAT_1:4;
then A3: A |^ (m * kl),(n * kl) c= A |^ (m * k),(n * l) by Th23;
x in A |^ (m * kl),(n * kl) by A2, Th40;
hence x in A |^ (m * k),(n * l) by A3; :: thesis: verum