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