let X be set ; :: thesis: for n being Nat
for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X
let n be Nat; :: thesis: for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X
let f be PartFunc of X,X; :: thesis: iter (f,n) is PartFunc of X,X
A1: field f = (dom f) \/ (rng f) ;
rng (iter (f,n)) c= field f by Th71;
then A2: rng (iter (f,n)) c= X by A1, XBOOLE_1:1;
dom (iter (f,n)) c= field f by Th71;
then dom (iter (f,n)) c= X by A1, XBOOLE_1:1;
hence iter (f,n) is PartFunc of X,X by A2, RELSET_1:4; :: thesis: verum