theorem :: FUNCT_7:78

for m, n being Nat
for R being Relation st n <> 0 holds
iter ((iter (R,m)),n) = iter (R,(m * n))