theorem :: NOMIN_3:16

for D being non empty set
for f being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & q ||= r & dom r c= dom q holds
<*p,f,r*> is SFHT of D