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;
now :: thesis: for x being object st x in (A *) + holds
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;
then A3: (A *) + c= A * ;
now :: thesis: for x being object st x in (A +) * holds
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;
then A5: (A +) * c= A * ;
A * c= (A *) + by Th59;
hence ( (A *) + = A * & (A +) * = A * ) by A1, A3, A5, XBOOLE_0:def 10; :: thesis: verum