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 Th70; :: thesis: verum