let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); :: thesis: for k, l, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n))
let k, l, m, n 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:12;
hence (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n)) by A2, FLANG_1:12; :: 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:12;
hence (A |^ (m,n)) ^^ (A |^ (k,l)) = (A |^ (k,l)) ^^ (A |^ (m,n)) by A3, FLANG_1:12; :: thesis: verum

end;

end;