let E be set ; :: thesis: for A being Subset of (E ^omega) holds (A ?) ^^ (A *) = A *
let A be Subset of (E ^omega); :: thesis: (A ?) ^^ (A *) = A *
thus (A ?) ^^ (A *) = ({(<%> E)} \/ A) ^^ (A *) by Th76
.= ({(<%> E)} ^^ (A *)) \/ (A ^^ (A *)) by FLANG_1:20
.= (A *) \/ (A ^^ (A *)) by FLANG_1:13
.= A * by FLANG_1:53, XBOOLE_1:12 ; :: thesis: verum