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 A2: A |^ m,n = {} by Th21;
then (A |^ m,n) ^^ (A |^ k,l) = {} by FLANG_1:13;
hence (A |^ m,n) ^^ (A |^ k,l) = (A |^ k,l) ^^ (A |^ m,n) by A2, FLANG_1:13; :: thesis: verum

end;

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

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

end;

end;