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 Th48;

A3: now :: thesis: for x being set st x in A * holds
( x in (A *) ^^ A & x in A ^^ (A *) )

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 Th41;

A5: now :: thesis: ( n = 0 implies ( x in (A *) ^^ A & x in A ^^ (A *) ) )

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

end;

A6: now :: thesis: ( n > 0 implies x in A ^^ (A *) )

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, Th50; :: thesis: verum

end;

now :: thesis: ( n > 0 implies x in (A *) ^^ A )

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, Th50; :: thesis: verum

end;

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

end;

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