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 * )
A1: A * c= (A + ) * by Th59, FLANG_1:62;

now

let x be set ; :: thesis: ( x in (A * ) + implies x in A * )
assume x in (A * ) + ; :: thesis: x in A *
then consider k being Nat such that
0 < k and
A2: x in (A * ) |^ k by Th48;
(A * ) |^ k c= A * by FLANG_1:66;
hence x in A * by A2; :: thesis: verum

end;

then A3: (A * ) + c= A * by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in (A + ) * implies x in A * )
assume x in (A + ) * ; :: thesis: x in A *
then consider k being Nat such that
A4: x in (A + ) |^ k by FLANG_1:42;
(A + ) |^ k c= A * by Th55, FLANG_1:60;
hence x in A * by A4; :: thesis: verum

end;

then A5: (A + ) * c= A * by TARSKI:def 3;
A * c= (A * ) + by Th59;
hence ( (A * ) + = A * & (A + ) * = A * ) by A1, A3, A5, XBOOLE_0:def 10; :: thesis: verum