let D be non empty set ; :: thesis: 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
let f be BinominativeFunction of D; :: thesis: for p, q being PartialPredicate of D st p is total holds
<*(PP_inversion p),f,q*> is SFHT of D
let p, q be PartialPredicate of D; :: thesis: ( p is total implies <*(PP_inversion p),f,q*> is SFHT of D )
assume p is total ; :: thesis: <*(PP_inversion p),f,q*> is SFHT of D
then A1: PP_inversion p ||= PP_False D by PARTPR_2:10;
<*(PP_False D),f,q*> is SFHT of D by Th18;
hence <*(PP_inversion p),f,q*> is SFHT of D by A1, Th15; :: thesis: verum