theorem Th74: :: FUNCT_7:75

for n being Nat
for R being Relation holds (id (field R)) * (iter (R,n)) = iter (R,n)