defpred S_{1}[ set ] means ex m being Nat st

( n <= m & $1 = A |^ m );

reconsider M = { B where B is Subset of (E ^omega) : S_{1}[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 m being Nat st

( n <= m & B = A |^ m ) } is Subset of (E ^omega) ; :: thesis: verum

( n <= m & $1 = A |^ m );

reconsider M = { B where B is Subset of (E ^omega) : S

union M is Subset of (E ^omega) ;

hence union { B where B is Subset of (E ^omega) : ex m being Nat st

( n <= m & B = A |^ m ) } is Subset of (E ^omega) ; :: thesis: verum