let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p being PartialPredicate of D holds <*(PP_False D),f,p*> is SFHT of D
let f be BinominativeFunction of D; :: thesis: for p being PartialPredicate of D holds <*(PP_False D),f,p*> is SFHT of D
let p be PartialPredicate of D; :: thesis: <*(PP_False D),f,p*> is SFHT of D
set F = PP_False D;
for d being Element of D st d in dom (PP_False D) & (PP_False D) . d = TRUE & d in dom f & f . d in dom p holds
p . (f . d) = TRUE by FUNCOP_1:7;
then <*(PP_False D),f,p*> in SFHTs D ;
hence <*(PP_False D),f,p*> is SFHT of D ; :: thesis: verum