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 (dom f) \/ (rng 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:76;
(iter f,(n + 1)) . x = (f * (iter f,n)) . x by FUNCT_7:73
.= f . (f,n -. x) by A1, A4, A5, FUNCT_1:23
.= f,(succ n) -. x by Th19
.= f,(n + 1) -. x by NAT_1:39 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(iter f,0 ) . x = (id ((dom f) \/ (rng f))) . x by FUNCT_7:70
.= x by A2, FUNCT_1:35
.= f,0 -. x by Th17 ;
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