let f be Function; :: thesis: ( rng f c= dom f implies iter (f,0) = id (dom f) )
assume rng f c= dom f ; :: thesis: iter (f,0) = id (dom f)
then field f = dom f by XBOOLE_1:12;
hence iter (f,0) = id (dom f) by FUNCT_7:68; :: thesis: verum