let E be set ; :: thesis: for A being Subset of (E ^omega) holds
( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )
let A be Subset of (E ^omega); :: thesis: ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )

A1: now

let x be set ; :: thesis: ( x in {(<%> E)} \/ ((A *) ^^ A) implies x in A * )
assume x in {(<%> E)} \/ ((A *) ^^ A) ; :: thesis: x in A *
then ( x in {(<%> E)} or x in (A *) ^^ A ) by XBOOLE_0:def 3;
then ( x = <%> E or x in A * ) by Th53, TARSKI:def 1;
hence x in A * by Th49; :: thesis: verum

end;

A2: now

let x be set ; :: thesis: ( x in A * implies x in {(<%> E)} \/ ((A *) ^^ A) )
assume x in A * ; :: thesis: x in {(<%> E)} \/ ((A *) ^^ A)
then consider n being Nat such that
A3: x in A |^ n by Th42;

A4: 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 A3, Th51; :: thesis: verum

end;

( n = 0 implies x in {(<%> E)} ) by A3, Th25;
hence x in {(<%> E)} \/ ((A *) ^^ A) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

A5: now

let x be set ; :: thesis: ( x in A * implies x in {(<%> E)} \/ (A ^^ (A *)) )
assume x in A * ; :: thesis: x in {(<%> E)} \/ (A ^^ (A *))
then consider n being Nat such that
A6: x in A |^ n by Th42;

A7: 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 A6, Th51; :: thesis: verum

end;

( n = 0 implies x in {(<%> E)} ) by A6, Th25;
hence x in {(<%> E)} \/ (A ^^ (A *)) by A7, XBOOLE_0:def 3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in {(<%> E)} \/ (A ^^ (A *)) implies x in A * )
assume x in {(<%> E)} \/ (A ^^ (A *)) ; :: thesis: x in A *
then ( x in {(<%> E)} or x in A ^^ (A *) ) by XBOOLE_0:def 3;
then ( x = <%> E or x in A * ) by Th53, TARSKI:def 1;
hence x in A * by Th49; :: thesis: verum

end;

hence ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by A2, A5, A1, TARSKI:1; :: thesis: verum