let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds (A |^ m) |^ n = (A |^ n) |^ m
let m, n be Nat; :: thesis: (A |^ m) |^ n = (A |^ n) |^ m
thus (A |^ m) |^ n = A |^ (m * n) by FLANG_1:35
.= (A |^ n) |^ m by FLANG_1:35 ; :: thesis: verum