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 +) ^^ (A |^ (0,1)) by FLANG_2:79
.= (A |^ (0,1)) ^^ (A +) by Th72
.= (A ?) ^^ (A +) by FLANG_2:79 ; :: thesis: verum