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 |^.. 1) by Th50
.= (A |^.. 1) ^^ (A *) by Th32
.= (A +) ^^ (A *) by Th50 ; :: thesis: verum