let f be Function; :: thesis: for x being set st x in dom f holds
f orbit (f . x) c= f orbit x
let x be set ; :: thesis: ( x in dom f implies f orbit (f . x) c= f orbit x )
assume A1: x in dom f ; :: thesis: f orbit (f . x) c= f orbit x
let a be set ; :: according to TARSKI:def 3 :: thesis: ( a nin f orbit (f . x) or not a nin f orbit x )
assume a in f orbit (f . x) ; :: thesis: not a nin f orbit x
then consider n being Element of NAT such that
A2: a = (iter f,n) . (f . x) and
A3: f . x in dom (iter f,n) ;
A4: iter f,(n + 1) = (iter f,n) * f by FUNCT_7:71;
then A5: a = (iter f,(n + 1)) . x by A1, A2, FUNCT_1:23;
x in dom (iter f,(n + 1)) by A1, A3, A4, FUNCT_1:21;
hence not a nin f orbit x by A5; :: thesis: verum