let n be Element of NAT ; 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; 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; for x being Element of L holds (iter (f,n)) . x = (f,n) +. x
let x be Element of L; (iter (f,n)) . x = (f,n) +. x
defpred S1[ 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 for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A4:
S1[
n]
;
S1[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
S1[
n + 1]
;
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:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A3);
hence
(iter (f,n)) . x = (f,n) +. x
; verum