let E be set ; :: thesis: for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = (A *) ^^ (A ?)
let A be Subset of (E ^omega); :: thesis: (A ?) ^^ (A *) = (A *) ^^ (A ?)
thus (A ?) ^^ (A *) = (A |^ (0,1)) ^^ (A *) by Th79
.= (A *) ^^ (A |^ (0,1)) by Th66
.= (A *) ^^ (A ?) by Th79 ; :: thesis: verum