theorem Th76: :: FUNCT_7:77

for m, n being Nat
for R being Relation holds (iter (R,m)) * (iter (R,n)) = iter (R,(n + m))