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

A1: now :: thesis: for x being object st x in (A |^ k) ^^ (A |^ (m,n)) holds
x in (A |^ (m,n)) ^^ (A |^ k)

let x be object ; :: 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:17;
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 :: thesis: for x being object st x in (A |^ (m,n)) ^^ (A |^ k) holds
x in (A |^ k) ^^ (A |^ (m,n))

let x be object ; :: 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:17;
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