let f be Function; :: thesis: for x being set st x in dom f holds
f . x in f orbit x
let x be set ; :: thesis: ( x in dom f implies f . x in f orbit x )
assume A1: x in dom f ; :: thesis: f . x in f orbit x
iter f,1 = f by FUNCT_7:72;
hence f . x in f orbit x by A1; :: thesis: verum