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₁[ 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 :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be 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 (Segm n))) +. x by Th15
.= (f,(Segm (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 Th13 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A3);
hence (iter (f,n)) . x = (f,n) +. x ; :: thesis: verum