for X being set
for n being Nat holds iter ((id X),n) = id X