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

now

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 Th55;
hence A ^^ (A * ) = (A * ) ^^ A by A2, Th55; :: thesis: verum

end;

suppose A3: not <%> E in A ; :: thesis: A ^^ (A * ) = (A * ) ^^ A

then not <%> E in (A * ) ^^ A by Th16;
then A4: {(<%> E)} misses (A * ) ^^ A by ZFMISC_1:56;
not <%> E in A ^^ (A * ) by A3, Th16;
then {(<%> E)} misses A ^^ (A * ) by ZFMISC_1:56;
hence A ^^ (A * ) = (A * ) ^^ A by A1, A4, XBOOLE_1:71; :: thesis: verum

end;

end;

end;

hence A ^^ (A * ) = (A * ) ^^ A ; :: thesis: verum