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 FLANG_2:76
.= A * by Th53 ; :: thesis: (A ? ) + = A *
thus (A ? ) + = A * :: thesis: verum

proof

<%> E in A ? by FLANG_2:78;
then (A ? ) + = (A ? ) * by Th57;
hence (A ? ) + = A * by FLANG_2:85; :: thesis: verum

end;