theorem Th23: :: NOMIN_2:24

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