let X be set ; :: thesis: for n being Element of NAT
for f being PartFunc of , holds iter f,n is PartFunc of ,
let n be Element of NAT ; :: thesis: for f being PartFunc of , holds iter f,n is PartFunc of ,
let f be PartFunc of ,; :: thesis: iter f,n is PartFunc of ,
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 , by A1, RELSET_1:11; :: thesis: verum