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 (f,0) -. x = x

let f be Function of the carrier of L, the carrier of L; :: thesis: for x being Element of L holds (f,0) -. x = x

let x be Element of L; :: thesis: (f,0) -. x = 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 Def5;

thus H_{3}( 0 ) = x
from ORDINAL2:sch 8(A1); :: thesis: verum

for x being Element of L holds (f,0) -. x = x

let f be Function of the carrier of L, the carrier of L; :: thesis: for x being Element of L holds (f,0) -. x = x

let x be Element of L; :: thesis: (f,0) -. x = 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

thus H