theorem :: FUNCT_7:81

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