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