theorem :: NOMIN_2:22

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