theorem Th78: :: FUNCT_7:79

for m, n being Nat
for R being Relation st rng R c= dom R holds
iter ((iter (R,m)),n) = iter (R,(m * n))