theorem :: NOMIN_3:22

for n being Nat
for D being non empty set
for f being BinominativeFunction of D
for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds
<*p,(iter (f,n)),p*> is SFHT of D