let E be non empty set ; :: thesis: for f being Function of E,E
for x being Element of E holds (iter (f,0)) . x = x
let f be Function of E,E; :: thesis: for x being Element of E holds (iter (f,0)) . x = x
let x be Element of E; :: thesis: (iter (f,0)) . x = x
dom f = E by FUNCT_2:def 1;
then A1: x in (dom f) \/ (rng f) by XBOOLE_0:def 3;
thus (iter (f,0)) . x = (id (field f)) . x by FUNCT_7:68
.= x by A1, FUNCT_1:17 ; :: thesis: verum