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