let E be set ; 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); for k, m, n being Nat holds (A |^ k) |^ (m,n) c= (A |^ (m,n)) |^ k
let k, m, n be Nat; (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; verum