theorem :: NOMIN_4:5

for v being object
for V, A being set
for f being SCBinominativeFunction of V,A st A is_without_nonatomicND_wrt V holds
for d being NonatomicND of V,A st v in V & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}