let f be Function; :: thesis: for x being set st x in dom f holds
x in f orbit x
let x be set ; :: thesis: ( x in dom f implies x in f orbit x )
assume x in dom f ; :: thesis: x in f orbit x
then A1: x in (dom f) \/ (rng f) by XBOOLE_0:def 3;
A2: iter f,0 = id ((dom f) \/ (rng f)) by FUNCT_7:70;
then A3: (iter f,0 ) . x = x by A1, FUNCT_1:34;
dom (iter f,0 ) = (dom f) \/ (rng f) by A2, FUNCT_1:34;
hence x in f orbit x by A1, A3; :: thesis: verum