:: deftheorem Def3 defines FNDSC NOMIN_1:def 3 :
for V, A being set
for b₃ being Function holds
( b₃ = FNDSC (V,A) iff ( dom b₃ = NAT & b₃ . 0 = A & ( for n being Nat holds b₃ . (n + 1) = NDSS (V,(A \/ (b₃ . n))) ) ) );