let R be Relation; :: thesis: ( rng R c= dom R implies iter (R,0) = id (dom R) )
assume rng R c= dom R ; :: thesis: iter (R,0) = id (dom R)
then field R = dom R by XBOOLE_1:12;
hence iter (R,0) = id (dom R) by Th67; :: thesis: verum