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