theorem Th27: :: NOMIN_3:28

for V, A being set
for p, q being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE ) holds
<*p,f,q*> is SFHT of (ND (V,A))