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 & x in dom (iter f,n) ) ;
A3: iter f,(n + 1) = f * (iter f,n) by FUNCT_7:73;
then A4: f . y = (iter f,(n + 1)) . x by A2, FUNCT_1:23;
( y in rng (iter f,n) & rng (iter f,n) c= (dom f) \/ (rng f) & (dom f) \/ (rng f) = dom f ) by A1, A2, FUNCT_1:def 5, FUNCT_7:74, XBOOLE_1:12;
then x in dom (iter f,(n + 1)) by A2, A3, FUNCT_1:21;
hence f . y in f orbit x by A4; :: thesis: verum