defpred S₁[ set ] means ex n being Nat st $1 = A |^ n;
reconsider M = { B where B is Subset of (E ^omega ) : S₁[B] } as Subset-Family of (E ^omega ) from DOMAIN_1:sch 7();
union M is Subset of (E ^omega ) ;
hence union { B where B is Subset of (E ^omega ) : ex n being Nat st B = A |^ n } is Subset of (E ^omega ) ; :: thesis: verum