consider f being Function such that
A1: ( dom f = NAT & f . 0 = X & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) ) from NAT_1:sch 11();
take UNI = union (rng f); :: thesis:
let x be set ; :: thesis:
thus ( x in UNI implies ex f being Function ex n being Element of NAT st
( x in f . n & dom f = NAT & f . 0 = X & ( for k being Nat holds f . (k + 1) = union (f . k) ) ) ) :: thesis:

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

end;

deffunc H₃( set , set ) -> set = union $2;
given g being Function, n being Element of NAT such that A7: x in g . n and
A8: dom g = NAT and
A9: g . 0 = X and
A10: for k being Nat holds g . (k + 1) = H₃(k,g . k) ; :: thesis:
A11: dom f = NAT by A1;
A12: f . 0 = X by A1;
A13: for n being Nat holds f . (n + 1) = H₃(n,f . n) by A1;
A14: g = f from NAT_1:sch 15(A8, A9, A10, A11, A12, A13);
A15: g . n in rng f by A1, A14, FUNCT_1:def 5;
thus x in UNI by A7, A15, TARSKI:def 4; :: thesis: