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 Th49;
then A1: A * c= (A * ) ^^ (A * ) by Th17;
(A * ) ^^ (A * ) c= A * by Th47;
hence (A * ) ^^ (A * ) = A * by A1, XBOOLE_0:def 10; :: thesis: verum