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

defpred S_{1}[ Ordinal] means (f,$1) +. a is Element of L;

_{1}[ 0 ]
by Th13;

for O being Ordinal holds S_{1}[O]
from ORDINAL2:sch 1(A5, A1, A2);

hence (f,O) +. a is Element of L ; :: thesis: verum

defpred S

A1: now :: thesis: for O1 being Ordinal st S_{1}[O1] holds

S_{1}[ succ O1]

S

let O1 be Ordinal; :: thesis: ( S_{1}[O1] implies S_{1}[ succ O1] )

assume S_{1}[O1]
; :: thesis: S_{1}[ succ O1]

then reconsider fa = (f,O1) +. a as Element of L ;

f . fa = (f,(succ O1)) +. a by Th15;

hence S_{1}[ succ O1]
; :: thesis: verum

end;assume S

then reconsider fa = (f,O1) +. a as Element of L ;

f . fa = (f,(succ O1)) +. a by Th15;

hence S

A2: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{1}[O2] ) holds

S_{1}[O1]

A5:
SS

S

let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds

S_{1}[O2] ) implies S_{1}[O1] )

assume that

A3: ( O1 <> 0 & O1 is limit_ordinal ) and

for O2 being Ordinal st O2 in O1 holds

S_{1}[O2]
; :: thesis: S_{1}[O1]

consider Ls being Sequence such that

A4: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ls . O2 = H_{1}(O2) ) )
from ORDINAL2:sch 2();

(f,O1) +. a = "\/" ((rng Ls),L) by A3, A4, Th17;

hence S_{1}[O1]
; :: thesis: verum

end;S

assume that

A3: ( O1 <> 0 & O1 is limit_ordinal ) and

for O2 being Ordinal st O2 in O1 holds

S

consider Ls being Sequence such that

A4: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds

Ls . O2 = H

(f,O1) +. a = "\/" ((rng Ls),L) by A3, A4, Th17;

hence S

for O being Ordinal holds S

hence (f,O) +. a is Element of L ; :: thesis: verum