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 x in UNI ; :: thesis:
then consider Y being set such that
A2: ( x in Y & Y in rng f ) by TARSKI:def 4;
consider y being set such that
A3: ( y in dom f & Y = f . y ) by A2, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A1, A3;
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, A2, A3; :: thesis:

end;

deffunc H₃( set , set ) -> set = union $2;
given g being Function, n being Element of NAT such that A4: x in g . n and
A5: dom g = NAT and
B5: g . 0 = X and
C5: for k being Nat holds g . (k + 1) = H₃(k,g . k) ; :: thesis:
A6: dom f = NAT by A1;
B6: f . 0 = X by A1;
C6: for n being Nat holds f . (n + 1) = H₃(n,f . n) by A1;
g = f from NAT_1:sch 15(A5, B5, C5, A6, B6, C6);
then g . n in rng f by A1, FUNCT_1:def 5;
hence x in UNI by A4, TARSKI:def 4; :: thesis: