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