let E be set ; :: thesis:
let A be Subset of (E ^omega); :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume A1: x in (A +) + ; :: thesis:

per cases ;

suppose x = <%> E ; :: thesis:

hence x in A + by A1, Th56; :: thesis:

end;

suppose A2: x <> <%> E ; :: thesis:

(A +) + c= A * by Th55, Th61;
then x in A * by A1;
then A3: x in (A +) \/ {(<%> E)} by Th53;
not x in {(<%> E)} by A2, TARSKI:def 1;
hence x in A + by A3, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then A4: (A +) + c= A + ;
A + c= (A +) + by Th59;
hence (A +) + = A + by A4, XBOOLE_0:def 10; :: thesis: