theorem :: NOMIN_3:26

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