consider f being Function such that
A1:
( dom f = omega & f . 0 = X & ( for n being Nat holds f . (succ n) = H2(n,f . n) ) )
from ORDINAL2:sch 18();
take UNI = union (rng f); for x being object holds
( x in UNI iff 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) ) ) )
let x be object ; ( x in UNI iff 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) ) ) )
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) ) ) )
( 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) ) ) implies x in UNI )
deffunc H3( 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) = H3(k,g . k)
; x in UNI
A10:
dom f = omega
by A1;
A11:
f . 0 = X
by A1;
A12:
for n being Nat holds f . (succ n) = H3(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; verum