let X be set ; :: thesis: for n being Element of NAT
for f being PartFunc of X,X holds iter (f,n) is PartFunc of X,X
let n be Element of 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
A2: field f = (dom f) \/ (rng f) ;
rng (iter (f,n)) c= field f by Th74;
then A1: rng (iter (f,n)) c= X by A2, XBOOLE_1:1;
dom (iter (f,n)) c= field f by Th74;
then dom (iter (f,n)) c= X by A2, XBOOLE_1:1;
hence iter (f,n) is PartFunc of X,X by A1, RELSET_1:4; :: thesis: verum