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