let E be set ; :: thesis: for A being Subset of (E ^omega) holds (A *) ^^ (A *) = A *
let A be Subset of (E ^omega); :: thesis: (A *) ^^ (A *) = A *
<%> E in A * by Th48;
then A1: A * c= (A *) ^^ (A *) by Th16;
(A *) ^^ (A *) c= A * by Th46;
hence (A *) ^^ (A *) = A * by A1, XBOOLE_0:def 10; :: thesis: verum