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 ) by Lm1, Th70, XBOOLE_1:12;
hence iter f,0 = id X by FUNCT_2:67; :: thesis: verum