theorem :: NOMIN_3:29

for v being object
for V, A being set
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))