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 *
A1: A ^^ (A * ) c= A * by FLANG_1:54;
thus (A ? ) ^^ (A * ) = ({(<%> E)} \/ A) ^^ (A * ) by Th76
.= ({(<%> E)} ^^ (A * )) \/ (A ^^ (A * )) by FLANG_1:21
.= (A * ) \/ (A ^^ (A * )) by FLANG_1:14
.= A * by A1, XBOOLE_1:12 ; :: thesis: verum