theorem Th26: :: NOMIN_2:27

for a being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))