let X be set ; :: thesis: for m, n being Element of NAT
for f being Function of X,X holds iter (iter f,m),n = iter f,(m * n)
let m, n be Element of NAT ; :: thesis: for f being Function of X,X holds iter (iter f,m),n = iter f,(m * n)
let f be Function of X,X; :: thesis: iter (iter f,m),n = iter f,(m * n)
rng f c= dom f by Lm1;
hence iter (iter f,m),n = iter f,(m * n) by Th81; :: thesis: verum