defpred S₁[ set ] means ex n being Nat st
( n > 0 & $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
( n > 0 & B = A |^ n ) } is Subset of (E ^omega) ; :: thesis: verum