theorem :: NOMIN_2:33

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