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:71;
then A5: f . y = (iter (f,(n + 1))) . x by A2, A3, FUNCT_1:13;
A6: y in rng (iter (f,n)) by A2, A3, FUNCT_1:def 3;
A7: rng (iter (f,n)) c= field f by FUNCT_7:72;
field f = dom f by A1, XBOOLE_1:12;
then x in dom (iter (f,(n + 1))) by A2, A3, A4, A6, A7, FUNCT_1:11;
hence f . y in f orbit x by A5; :: thesis: verum