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