theorem Th73: :: FUNCT_7:74

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