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