let X be set ; :: thesis: for f being Function of X,X holds iter f,0 = id X
let f be Function of X,X; :: thesis: iter f,0 = id X
( iter f,0 = id ((dom f) \/ (rng f)) & (dom f) \/ (rng f) = dom f & dom f = X ) by Th70, Lm1, FUNCT_2:67, XBOOLE_1:12;
hence iter f,0 = id X ; :: thesis: verum