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