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