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_{1}[ 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;

.= x by A2, FUNCT_1:18

.= (f,0) +. x by Th13 ;

then A6: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A6, A3);

hence (iter (f,n)) . x = (f,n) +. x ; :: thesis: verum

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

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 :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

(iter (f,0)) . x =
(id (field f)) . x
by FUNCT_7:68
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[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 (Segm n))) +. x by Th15

.= (f,(Segm (n + 1))) +. x by NAT_1:38 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume A4: S

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 (Segm n))) +. x by Th15

.= (f,(Segm (n + 1))) +. x by NAT_1:38 ;

hence S

.= x by A2, FUNCT_1:18

.= (f,0) +. x by Th13 ;

then A6: S

for n being Nat holds S

hence (iter (f,n)) . x = (f,n) +. x ; :: thesis: verum