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

per cases ( ( m <= n & k <= l ) or m > n or k > l ) ;

suppose A1: ( m <= n & k <= l ) ; :: thesis: (A |^ m,n) ^^ (A |^ k,l) = (A |^ k,l) ^^ (A |^ m,n)

hence (A |^ m,n) ^^ (A |^ k,l) = A |^ (m + k),(n + l) by Th37
.= (A |^ k,l) ^^ (A |^ m,n) by A1, Th37 ;
:: thesis: verum

end;

suppose m > n ; :: thesis: (A |^ m,n) ^^ (A |^ k,l) = (A |^ k,l) ^^ (A |^ m,n)

then A |^ m,n = {} by Th21;
then ( (A |^ m,n) ^^ (A |^ k,l) = {} & (A |^ k,l) ^^ (A |^ m,n) = {} ) by FLANG_1:13;
hence (A |^ m,n) ^^ (A |^ k,l) = (A |^ k,l) ^^ (A |^ m,n) ; :: thesis: verum

end;

suppose k > l ; :: thesis: (A |^ m,n) ^^ (A |^ k,l) = (A |^ k,l) ^^ (A |^ m,n)

then A |^ k,l = {} by Th21;
then ( (A |^ m,n) ^^ (A |^ k,l) = {} & (A |^ k,l) ^^ (A |^ m,n) = {} ) by FLANG_1:13;
hence (A |^ m,n) ^^ (A |^ k,l) = (A |^ k,l) ^^ (A |^ m,n) ; :: thesis: verum

end;

end;