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 * ) ? = {(<%> E)} \/ (A * ) by Th76
.= A * by FLANG_1:49, ZFMISC_1:46 ; :: thesis: (A ? ) * = A *
thus (A ? ) * = ({(<%> E)} \/ A) * by Th76
.= A * by FLANG_1:49, FLANG_1:69 ; :: thesis: verum