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) & iter f,0 = id ((dom f) \/ (rng f)) ) by FUNCT_7:70, XBOOLE_0:def 3;
then ( (iter f,0 ) . x = x & dom (iter f,0 ) = (dom f) \/ (rng f) ) by FUNCT_1:34;
hence x in f orbit x by A1; :: thesis: verum