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