:: deftheorem Def6 defines -NonatomicND-yielding NOMIN_7:def 6 :
for V, A being set
for f being FinSequence holds
( f is V,A -NonatomicND-yielding iff for n being Nat st 1 <= n & n <= len f holds
f . n is NonatomicND of V,A );