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