theorem :: FUNCT_7:85

for X being set
for m, n being Nat
for f being Function of X,X holds iter ((iter (f,m)),n) = iter (f,(m * n))