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 (field f) & field f = dom f ) by Lm1, Th67, XBOOLE_1:12;
hence iter (f,0) = id X by FUNCT_2:52; :: thesis: verum