let f be Function; :: thesis: for x being set st x in dom f & f . x in dom f holds
f orbit (f . x) c= f orbit x
let x be set ; :: thesis: ( x in dom f & f . x in dom f implies f orbit (f . x) c= f orbit x )
assume A1: ( x in dom f & f . 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) & f . x in dom (iter f,n) ) ;
iter f,(n + 1) = (iter f,n) * f by FUNCT_7:71;
then ( a = (iter f,(n + 1)) . x & x in dom (iter f,(n + 1)) ) by A1, A2, FUNCT_1:21, FUNCT_1:23;
hence not a nin f orbit x ; :: thesis: verum