let L be Lattice; :: thesis: for f being Function of the carrier of L, the carrier of L

for x being Element of L

for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)

let f be Function of the carrier of L, the carrier of L; :: thesis: for x being Element of L

for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)

let x be Element of L; :: thesis: for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)

let O be Ordinal; :: thesis: (f,(succ O)) +. x = f . ((f,O) +. x)

deffunc H_{1}( Ordinal, set ) -> set = f . $2;

deffunc H_{2}( Ordinal, Sequence) -> Element of the carrier of L = "\/" ((rng $2),L);

deffunc H_{3}( Ordinal) -> set = (f,$1) +. x;

A1: for O being Ordinal

for y being object holds

( y = H_{3}(O) iff ex L0 being Sequence st

( y = last L0 & dom L0 = succ O & L0 . 0 = x & ( for C being Ordinal st succ C in succ O holds

L0 . (succ C) = H_{1}(C,L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds

L0 . C = H_{2}(C,L0 | C) ) ) )
by Def4;

for O being Ordinal holds H_{3}( succ O) = H_{1}(O,H_{3}(O))
from ORDINAL2:sch 9(A1);

hence (f,(succ O)) +. x = f . ((f,O) +. x) ; :: thesis: verum

for x being Element of L

for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)

let f be Function of the carrier of L, the carrier of L; :: thesis: for x being Element of L

for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)

let x be Element of L; :: thesis: for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)

let O be Ordinal; :: thesis: (f,(succ O)) +. x = f . ((f,O) +. x)

deffunc H

deffunc H

deffunc H

A1: for O being Ordinal

for y being object holds

( y = H

( y = last L0 & dom L0 = succ O & L0 . 0 = x & ( for C being Ordinal st succ C in succ O holds

L0 . (succ C) = H

L0 . C = H

for O being Ordinal holds H

hence (f,(succ O)) +. x = f . ((f,O) +. x) ; :: thesis: verum