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