deffunc H₁( 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₁(n,F . n) ) ) from NAT_1:sch 11();
hence ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = A & ( for n being Nat holds b₁ . (n + 1) = NDSS (V,(A \/ (b₁ . n))) ) ) ; :: thesis: verum