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

( (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