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
(A * ) ^^ A = A |^.. 1 by Th30;
hence A + = (A * ) ^^ A by Th50; :: thesis: verum