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 :: thesis: for x being object st x in {(<%> E)} \/ ((A *) ^^ A) holds
x in A *
let x be object ; :: 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 Th52, TARSKI:def 1;
hence x in A * by Th48; :: thesis: verum
end;
A2: now :: thesis: for x being object st x in A * holds
x in {(<%> E)} \/ ((A *) ^^ A)
let x be object ; :: 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 Th41;
A4: 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 A3, Th50; :: thesis: verum
end;
( n = 0 implies x in {(<%> E)} ) by A3, Th24;
hence x in {(<%> E)} \/ ((A *) ^^ A) by A4, XBOOLE_0:def 3; :: thesis: verum
end;
A5: now :: thesis: for x being object st x in A * holds
x in {(<%> E)} \/ (A ^^ (A *))
let x be object ; :: 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 Th41;
A7: 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 A6, Th50; :: thesis: verum
end;
( n = 0 implies x in {(<%> E)} ) by A6, Th24;
hence x in {(<%> E)} \/ (A ^^ (A *)) by A7, XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: for x being object st x in {(<%> E)} \/ (A ^^ (A *)) holds
x in A *
let x be object ; :: 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 Th52, TARSKI:def 1;
hence x in A * by Th48; :: thesis: verum
end;
hence ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by A2, A5, A1, TARSKI:2; :: thesis: verum