theorem :: FUNCT_7:86

for X being set
for n being Nat
for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X