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