consider f being Function such that
A1: ( dom f = omega & f . 0 = X & ( for n being Nat holds f . (succ n) = H₂(n,f . n) ) ) from ORDINAL2:sch 18();
take UNI = union (rng f); :: thesis:
let x be object ; :: thesis:
thus ( x in UNI implies ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) :: thesis:

assume x in UNI ; :: thesis:
then consider Y being set such that
A2: x in Y and
A3: Y in rng f by TARSKI:def 4;
consider y being object such that
A4: y in dom f and
A5: Y = f . y by A3, FUNCT_1:def 3;
reconsider y = y as Element of omega by A1, A4;
take f ; :: thesis:
take y ; :: thesis:
thus ( x in f . y & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) by A1, A2, A5; :: thesis:

end;

deffunc H₃( set , set ) -> set = union $2;
given g being Function, n being Element of omega such that A6: x in g . n and
A7: dom g = omega and
A8: g . 0 = X and
A9: for k being Nat holds g . (succ k) = H₃(k,g . k) ; :: thesis:
A10: dom f = omega by A1;
A11: f . 0 = X by A1;
A12: for n being Nat holds f . (succ n) = H₃(n,f . n) by A1;
g = f from ORDINAL2:sch 20(A7, A8, A9, A10, A11, A12);
then g . n in rng f by A1, FUNCT_1:def 3;
hence x in UNI by A6, TARSKI:def 4; :: thesis: