let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
let m, n be Nat; :: thesis: (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
(A |^ (0,1)) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A |^ (0,1)) by Th39;
then (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A |^ (0,1)) by Th79;
hence (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?) by Th79; :: thesis: verum