theorem Th68: :: FUNCT_7:69

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