deffunc H_{1}( set , set ) -> set = NDSS (V,(A \/ $2));

ex F being Function st

( dom F = NAT & F . 0 = A & ( for n being Nat holds F . (n + 1) = H_{1}(n,F . n) ) )
from NAT_1:sch 11();

hence ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = A & ( for n being Nat holds b_{1} . (n + 1) = NDSS (V,(A \/ (b_{1} . n))) ) )
; :: thesis: verum

ex F being Function st

( dom F = NAT & F . 0 = A & ( for n being Nat holds F . (n + 1) = H

hence ex b

( dom b