let f be Function; :: thesis: iter f,1 = f
thus iter f,1 = iter f,(0 + 1)
.= (iter f,0 ) * f by Th71
.= (id ((dom f) \/ (rng f))) * f by Th70
.= f by Lm3 ; :: thesis: verum