theorem :: FUNCT_7:88

for f being Function
for n being Nat holds iter (f,n) = compose ((n |-> f),(field f))