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 (field f) by FUNCT_7:68;
then A3: (iter (f,0)) . x = x by A1, FUNCT_1:17;
dom (iter (f,0)) = (dom f) \/ (rng f) by A2;
hence x in f orbit x by A1, A3; :: thesis: verum