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 *
<%> E in A ? by FLANG_2:78;
then (A ?) + = (A ?) * by Th57;
hence (A ?) + = A * by FLANG_2:85; :: thesis: verum