let E be set ; 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); for m, n being Nat holds (A ?) ^^ (A |^ (m,n)) = (A |^ (m,n)) ^^ (A ?)
let m, n be Nat; (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; verum