let n be Element of NAT ; :: thesis: for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let L be Lattice; :: thesis: for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let f be Function of the carrier of L, the carrier of L; :: thesis: for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let x be Element of L; :: thesis: (iter (f,n)) . x = (f,n) +. x
defpred S₁[ Element of NAT ] means (iter (f,$1)) . x = (f,$1) +. x;
A1: dom f = the carrier of L by FUNCT_2:def 1;
then A2: x in field f by XBOOLE_0:def 3;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
rng f c= the carrier of L ;
then A5: dom (iter (f,n)) = dom f by A1, FUNCT_7:74;
(iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71
.= f . ((f,n) +. x) by A1, A4, A5, FUNCT_1:13
.= (f,(succ n)) +. x by Th18
.= (f,(n + 1)) +. x by NAT_1:38 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(iter (f,0)) . x = (id (field f)) . x by FUNCT_7:68
.= x by A2, FUNCT_1:18
.= (f,0) +. x by Th16 ;
then A6: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A3);
hence (iter (f,n)) . x = (f,n) +. x ; :: thesis: verum