let X be set ; :: thesis: for m, n being Nat
for f being Function of X,X holds iter ((iter (f,m)),n) = iter (f,(m * n))
let m, n be 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 Th78; :: thesis: verum