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:61;

A * c= (A *) + by Th59;

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

( (A *) + = A * & (A +) * = A * )

let A be Subset of (E ^omega); :: thesis: ( (A *) + = A * & (A +) * = A * )

A1: A * c= (A +) * by Th59, FLANG_1:61;

now :: thesis: for x being object st x in (A *) + holds

x in A *

then A3:
(A *) + c= A *
;x in A *

let x be object ; :: 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:65;

hence x in A * by A2; :: thesis: verum

end;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:65;

hence x in A * by A2; :: thesis: verum

now :: thesis: for x being object st x in (A +) * holds

x in A *

then A5:
(A +) * c= A *
;x in A *

let x be object ; :: 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:41;

(A +) |^ k c= A * by Th55, FLANG_1:59;

hence x in A * by A4; :: thesis: verum

end;assume x in (A +) * ; :: thesis: x in A *

then consider k being Nat such that

A4: x in (A +) |^ k by FLANG_1:41;

(A +) |^ k c= A * by Th55, FLANG_1:59;

hence x in A * by A4; :: thesis: verum

A * c= (A *) + by Th59;

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