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 object ; :: 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:69;
then A5: a = (iter (f,(n + 1))) . x by A1, A2, FUNCT_1:13;
x in dom (iter (f,(n + 1))) by A1, A3, A4, FUNCT_1:11;
hence not a nin f orbit x by A5; :: thesis: verum