let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p being PartialPredicate of D holds <*{},f,p*> in SFHTs D
let f be BinominativeFunction of D; :: thesis: for p being PartialPredicate of D holds <*{},f,p*> in SFHTs D
let p be PartialPredicate of D; :: thesis: <*{},f,p*> in SFHTs D
A1: {} is PartialPredicate of D by RELSET_1:12;
for d being Element of D st d in dom {} & {} . d = TRUE & d in dom f & f . d in dom p holds
p . (f . d) = TRUE ;
hence <*{},f,p*> in SFHTs D by A1; :: thesis: verum