let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
let A be Subset of (E ^omega); :: thesis: for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
let k, m, n be Nat; :: thesis: (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
(A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) by Th40;
hence (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k by Th42; :: thesis: verum