for V, A being set
for d being TypeSCNominativeData of V,A
for g being b₁,b₂ -FPrg-yielding FinSequence
for X being b₁ -valued one-to-one FinSequence st dom g = dom X & d in_doms g holds
NDentry (g,X,d) is NonatomicND of V,A