theorem :: NOMIN_3:13

for D being non empty set
for p being PartialPredicate of D holds <*p,(id (dom p)),p*> is SFHT of D