theorem :: NOMIN_3:30

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_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A))