theorem Th7: :: ABIAN:7

for E being non empty set
for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c
for n being Nat holds (iter (f,n)) . e in c