:: deftheorem defines orbit AOFA_000:def 5 :
for f being Function
for x being object holds f orbit x = { ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } ;