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

A1: now

let x be set ; :: thesis: ( x in (A |^ k) ^^ (A |^ m,n) implies x in (A |^ m,n) ^^ (A |^ k) )
assume x in (A |^ k) ^^ (A |^ m,n) ; :: thesis: x in (A |^ m,n) ^^ (A |^ k)
then consider a, b being Element of E ^omega such that
A2: a in A |^ k and
A3: b in A |^ m,n and
A4: x = a ^ b by FLANG_1:def 1;
consider mn being Nat such that
A5: ( m <= mn & mn <= n ) and
A6: b in A |^ mn by A3, Th19;
A |^ mn c= A |^ m,n by A5, Th20;
then A7: (A |^ mn) ^^ (A |^ k) c= (A |^ m,n) ^^ (A |^ k) by FLANG_1:18;
a ^ b in (A |^ k) ^^ (A |^ mn) by A2, A6, FLANG_1:def 1;
then a ^ b in (A |^ mn) ^^ (A |^ k) by Th12;
hence x in (A |^ m,n) ^^ (A |^ k) by A4, A7; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in (A |^ m,n) ^^ (A |^ k) implies x in (A |^ k) ^^ (A |^ m,n) )
assume x in (A |^ m,n) ^^ (A |^ k) ; :: thesis: x in (A |^ k) ^^ (A |^ m,n)
then consider a, b being Element of E ^omega such that
A8: a in A |^ m,n and
A9: b in A |^ k and
A10: x = a ^ b by FLANG_1:def 1;
consider mn being Nat such that
A11: ( m <= mn & mn <= n ) and
A12: a in A |^ mn by A8, Th19;
A |^ mn c= A |^ m,n by A11, Th20;
then A13: (A |^ k) ^^ (A |^ mn) c= (A |^ k) ^^ (A |^ m,n) by FLANG_1:18;
a ^ b in (A |^ mn) ^^ (A |^ k) by A9, A12, FLANG_1:def 1;
then a ^ b in (A |^ k) ^^ (A |^ mn) by Th12;
hence x in (A |^ k) ^^ (A |^ m,n) by A10, A13; :: thesis: verum

end;

hence (A |^ m,n) ^^ (A |^ k) = (A |^ k) ^^ (A |^ m,n) by A1, TARSKI:2; :: thesis: verum