for D being non empty set
for f being BinominativeFunction of D
for p, q being PartialPredicate of D st p is total holds
<*(PP_inversion p),f,q*> is SFHT of D