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