let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
let A be Subset of (E ^omega); :: thesis: for k, l, m, n being Nat holds (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
let k, l, m, n be Nat; :: thesis: (A |^ (m,n)) |^ (k,l) c= A |^ ((m * k),(n * l))
let x be object ; :: 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