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 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 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 Nat holds (iter (f,n)) . e in c
let e be Element of c; :: thesis: for n being Nat holds (iter (f,n)) . e in c
let n be Nat; :: thesis: (iter (f,n)) . e in c
dom f = E by FUNCT_2:def 1;
then (iter (f,n)) . e in (dom f) \/ (rng f) by XBOOLE_0:def 3;
then (iter (f,n)) . e = (id (field f)) . ((iter (f,n)) . e) by FUNCT_1:17
.= (iter (f,0)) . ((iter (f,n)) . e) by FUNCT_7:68 ;
then A1: [((iter (f,n)) . e),e] in =_ f by Def7;
ex x9 being object st
( x9 in E & c = Class ((=_ f),x9) ) by EQREL_1:def 3;
then c = Class ((=_ f),e) by EQREL_1:23;
hence (iter (f,n)) . e in c by A1, EQREL_1:19; :: thesis: verum