let E be set ; :: thesis: for A being Subset of (E ^omega) holds A ^^ (A *) = (A *) ^^ A
let A be Subset of (E ^omega); :: thesis: A ^^ (A *) = (A *) ^^ A
A1: ( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) ) by Th56;
now :: thesis: A ^^ (A *) = (A *) ^^ A
per cases ( <%> E in A or not <%> E in A ) ;
suppose A2: <%> E in A ; :: thesis: A ^^ (A *) = (A *) ^^ A
then A * = A ^^ (A *) by Th54;
hence A ^^ (A *) = (A *) ^^ A by A2, Th54; :: thesis: verum
end;
suppose A3: not <%> E in A ; :: thesis: A ^^ (A *) = (A *) ^^ A
then not <%> E in (A *) ^^ A by Th15;
then A4: {(<%> E)} misses (A *) ^^ A by ZFMISC_1:50;
not <%> E in A ^^ (A *) by A3, Th15;
then {(<%> E)} misses A ^^ (A *) by ZFMISC_1:50;
hence A ^^ (A *) = (A *) ^^ A by A1, A4, XBOOLE_1:71; :: thesis: verum
end;
end;
end;
hence A ^^ (A *) = (A *) ^^ A ; :: thesis: verum