let R be Relation; :: thesis: ( rng R misses dom R implies iter (R,2) = {} )
assume A1: rng R misses dom R ; :: thesis: iter (R,2) = {}
thus iter (R,2) = iter (R,(1 + 1))
.= (iter (R,1)) * R by Th70
.= R * R by Th69
.= {} by A1, RELAT_1:44 ; :: thesis: verum