let f be Function; :: thesis: for x, y being set st rng f c= dom f & y in f orbit x holds
f . y in f orbit x
let x, y be set ; :: thesis: ( rng f c= dom f & y in f orbit x implies f . y in f orbit x )
assume A1: rng f c= dom f ; :: thesis: ( not y in f orbit x or f . y in f orbit x )
assume y in f orbit x ; :: thesis: f . y in f orbit x
then consider n being Element of NAT such that
A2: y = (iter f,n) . x and
A3: x in dom (iter f,n) ;
A4: iter f,(n + 1) = f * (iter f,n) by FUNCT_7:73;
then A5: f . y = (iter f,(n + 1)) . x by A2, A3, FUNCT_1:23;
A6: y in rng (iter f,n) by A2, A3, FUNCT_1:def 5;
A7: rng (iter f,n) c= (dom f) \/ (rng f) by FUNCT_7:74;
(dom f) \/ (rng f) = dom f by A1, XBOOLE_1:12;
then x in dom (iter f,(n + 1)) by A2, A3, A4, A6, A7, FUNCT_1:21;
hence f . y in f orbit x by A5; :: thesis: verum