let X be set ; :: thesis: for f being Function of X,X
for n being Nat holds iter (f,n) is Function of X,X
let f be Function of X,X; :: thesis: for n being Nat holds iter (f,n) is Function of X,X
let n be Nat; :: thesis: iter (f,n) is Function of X,X
A1: ( X = {} implies X = {} ) ;
then A2: ( dom f = X & rng f c= X ) by FUNCT_2:def 1;
then ( dom (iter (f,n)) = X & rng (iter (f,n)) c= X ) by Lemiter02;
then reconsider R = iter (f,n) as Relation of X,X by RELSET_1:11;
( dom R = X & rng R c= X ) by A2, Lemiter02;
hence iter (f,n) is Function of X,X by A1, FUNCT_2:def 1; :: thesis: verum