theorem Th3: :: ABIAN:3

for E being non empty set
for f being Function of E,E
for x being Element of E holds (iter (f,0)) . x = x