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