let E be set ; :: thesis: for A being Subset of (E ^omega ) st <%> E in A holds
( A * = (A * ) ^^ A & A * = A ^^ (A * ) )
let A be Subset of (E ^omega ); :: thesis: ( <%> E in A implies ( A * = (A * ) ^^ A & A * = A ^^ (A * ) ) )
assume A1: <%> E in A ; :: thesis: ( A * = (A * ) ^^ A & A * = A ^^ (A * ) )
A2: <%> E in A * by Th49;

A3: now

let x be set ; :: thesis: ( x in A * implies ( x in (A * ) ^^ A & x in A ^^ (A * ) ) )
assume x in A * ; :: thesis: ( x in (A * ) ^^ A & x in A ^^ (A * ) )
then consider n being Nat such that
A4: x in A |^ n by Th42;

A5: now

assume n = 0 ; :: thesis: ( x in (A * ) ^^ A & x in A ^^ (A * ) )
then x in {(<%> E)} by A4, Th25;
then x = <%> E by TARSKI:def 1;
hence ( x in (A * ) ^^ A & x in A ^^ (A * ) ) by A1, A2, Th16; :: thesis: verum

end;

A6: now

assume n > 0 ; :: thesis: x in A ^^ (A * )
then ex m being Nat st m + 1 = n by NAT_1:6;
hence x in A ^^ (A * ) by A4, Th51; :: thesis: verum

end;

now

assume n > 0 ; :: thesis: x in (A * ) ^^ A
then ex m being Nat st m + 1 = n by NAT_1:6;
hence x in (A * ) ^^ A by A4, Th51; :: thesis: verum

end;

hence ( x in (A * ) ^^ A & x in A ^^ (A * ) ) by A5, A6; :: thesis: verum

end;

then A7: for x being set st x in A * holds
x in (A * ) ^^ A ;
A8: for x being set st x in A * holds
x in A ^^ (A * ) by A3;
for x being set holds
( ( x in (A * ) ^^ A implies x in A * ) & ( x in A ^^ (A * ) implies x in A * ) ) by Th53;
hence ( A * = (A * ) ^^ A & A * = A ^^ (A * ) ) by A7, A8, TARSKI:2; :: thesis: verum