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
A1:
dom f = the carrier of L
by FUNCT_2:def 1;
then A2:
x in (dom f) \/ (rng f)
by XBOOLE_0:def 3;
defpred S1[ Element of NAT ] means (iter f,$1) . x = f,$1 +. x;
(iter f,0 ) . x =
(id ((dom f) \/ (rng f))) . x
by FUNCT_7:70
.=
x
by A2, FUNCT_1:35
.=
f,0 +. x
by Th16
;
then A3:
S1[ 0 ]
;
A4:
now let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )assume A5:
S1[
n]
;
:: thesis: S1[n + 1]
rng f c= the
carrier of
L
;
then A6:
dom (iter f,n) = dom f
by A1, FUNCT_7:76;
(iter f,(n + 1)) . x =
(f * (iter f,n)) . x
by FUNCT_7:73
.=
f . (f,n +. x)
by A1, A5, A6, FUNCT_1:23
.=
f,
(succ n) +. x
by Th18
.=
f,
(n + 1) +. x
by NAT_1:39
;
hence
S1[
n + 1]
;
:: thesis: verum end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A3, A4);
hence
(iter f,n) . x = f,n +. x
; :: thesis: verum