theorem :: NOMIN_2:29

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