theorem :: NOMIN_2:30

for a, b, c being object
for V, A being set
for d being TypeSCNominativeData of V,A
for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds
NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A