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
rng (iter (f,n)) c= (dom f) \/ (rng f) by Th74;
then A1: rng (iter (f,n)) c= X by XBOOLE_1:1;
dom (iter (f,n)) c= (dom f) \/ (rng f) by Th74;
then dom (iter (f,n)) c= X by XBOOLE_1:1;
hence iter (f,n) is PartFunc of X,X by A1, RELSET_1:11; :: thesis: verum