let E be non empty set ; :: thesis: for f being Function of E,E
for c being Element of Class (=_ f)
for e being Element of c
for n being Element of NAT holds (iter f,n) . e in c
let f be Function of E,E; :: thesis: for c being Element of Class (=_ f)
for e being Element of c
for n being Element of NAT holds (iter f,n) . e in c
let c be Element of Class (=_ f); :: thesis: for e being Element of c
for n being Element of NAT holds (iter f,n) . e in c
let e be Element of c; :: thesis: for n being Element of NAT holds (iter f,n) . e in c
let n be Element of NAT ; :: thesis: (iter f,n) . e in c
( dom f = E & rng f c= E ) by FUNCT_2:def 1, RELAT_1:def 19;
then A1: (iter f,n) . e in (dom f) \/ (rng f) by XBOOLE_0:def 3;
consider x' being set such that
A2: ( x' in E & c = Class (=_ f),x' ) by EQREL_1:def 5;
A3: c = Class (=_ f),e by A2, EQREL_1:31;
(iter f,n) . e = (id ((dom f) \/ (rng f))) . ((iter f,n) . e) by A1, FUNCT_1:34
.= (iter f,0 ) . ((iter f,n) . e) by FUNCT_7:70 ;
then [((iter f,n) . e),e] in =_ f by Def7;
hence (iter f,n) . e in c by A3, EQREL_1:27; :: thesis: verum