theorem Th22: :: NOMIN_2:23

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