:: deftheorem defines -NonatomicND-yielding NOMIN_7:def 5 :
for V, A being set
for f being Function holds
( f is V,A -NonatomicND-yielding iff for n being object st n in dom f holds
f . n is NonatomicND of V,A );