let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m
let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m
let m, n be Nat; :: thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m

per cases ( m > 0 or m <= 0 ) ;

suppose A1: m > 0 ; :: thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m

(A |^ m) |^.. n c= A |^.. (m * n) by Th35;
hence (A |^ m) |^.. n c= (A |^.. n) |^ m by A1, Th19; :: thesis: verum

end;

suppose m <= 0 ; :: thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m

then A2: m = 0 ;
then (A |^ m) |^.. n = {(<%> E)} |^.. n by FLANG_1:24
.= {(<%> E)} by Th15
.= (A |^.. n) |^ m by A2, FLANG_1:24 ;
hence (A |^ m) |^.. n c= (A |^.. n) |^ m ; :: thesis: verum

end;

end;