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 (dom f) \/ (rng f) = dom f by XBOOLE_1:12;
hence iter (f,0) = id (dom f) by FUNCT_7:70; :: thesis: verum