let D be non empty set ; :: thesis: for f being BinominativeFunction of D
for p being PartialPredicate of D holds <*p,(id (field f)),p*> is SFHT of D
let f be BinominativeFunction of D; :: thesis: for p being PartialPredicate of D holds <*p,(id (field f)),p*> is SFHT of D
let p be PartialPredicate of D; :: thesis: <*p,(id (field f)),p*> is SFHT of D
set i = id (field f);
A1: id (field f) is BinominativeFunction of D by PARTPR_2:5;
for d being Element of D st d in dom p & p . d = TRUE & d in dom (id (field f)) & (id (field f)) . d in dom p holds
p . ((id (field f)) . d) = TRUE by FUNCT_1:17;
then <*p,(id (field f)),p*> in SFHTs D by A1;
hence <*p,(id (field f)),p*> is SFHT of D ; :: thesis: verum