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