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

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

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

for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

let x be Element of L; :: thesis: for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

let O be Ordinal; :: thesis: for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

let T be Sequence; :: thesis: ( O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) implies (f,O) +. x = "\/" ((rng T),L) )

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;

assume that

A1: ( O <> 0 & O is limit_ordinal ) and

A2: dom T = O and

A3: for A being Ordinal st A in O holds

T . A = H_{3}(A)
; :: thesis: (f,O) +. x = "\/" ((rng T),L)

A4: 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;

thus H_{3}(O) = H_{2}(O,T)
from ORDINAL2:sch 10(A4, A1, A2, A3); :: thesis: verum

for x being Element of L

for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

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

for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

let x be Element of L; :: thesis: for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

let O be Ordinal; :: thesis: for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) holds

(f,O) +. x = "\/" ((rng T),L)

let T be Sequence; :: thesis: ( O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds

T . A = (f,A) +. x ) implies (f,O) +. x = "\/" ((rng T),L) )

deffunc H

deffunc H

deffunc H

assume that

A1: ( O <> 0 & O is limit_ordinal ) and

A2: dom T = O and

A3: for A being Ordinal st A in O holds

T . A = H

A4: 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

thus H