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 A * implies x in {(<%> E)} \/ ((A * ) ^^ A) )
assume x in A * ; :: thesis: x in {(<%> E)} \/ ((A * ) ^^ A)
then consider n being Nat such that
A2: x in A |^ n by Th42;
A3: ( n = 0 implies x in {(<%> E)} ) by A2, Th25;

now

assume n > 0 ; :: thesis: x in (A * ) ^^ A
then consider m being Nat such that
A4: m + 1 = n by NAT_1:6;
thus x in (A * ) ^^ A by A2, A4, Th51; :: thesis: verum

end;

hence x in {(<%> E)} \/ ((A * ) ^^ A) by A3, 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: ( n = 0 implies x in {(<%> E)} ) by A6, Th25;

now

assume n > 0 ; :: thesis: x in A ^^ (A * )
then consider m being Nat such that
A8: m + 1 = n by NAT_1:6;
thus x in A ^^ (A * ) by A6, A8, Th51; :: thesis: verum

end;

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

end;

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

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 A1, A5, A9, TARSKI:2; :: thesis: verum