theorem :: NOMIN_2:21

for f being Function
for a, d being object holds NDentry (<*f*>,<*a*>,d) = {[a,(f . d)]}