theorem :: NOMIN_3:21

for D being non empty set
for f, g being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*(PP_and (r,p)),f,q*> is SFHT of D & <*(PP_and ((PP_not r),p)),g,q*> is SFHT of D holds
<*p,(PP_IF (r,f,g)),q*> is SFHT of D