theorem Th70: :: FUNCT_7:71

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