let f be Function; :: thesis: ( rng f misses dom f implies iter (f,2) = {} )
assume A1: rng f misses dom f ; :: thesis: iter (f,2) = {}
thus iter (f,2) = iter (f,(1 + 1))
.= (iter (f,1)) * f by Th71
.= f * f by Th72
.= {} by A1, RELAT_1:67 ; :: thesis: verum