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