deffunc H₁( Ordinal) -> set = (f,$1) +. a;
defpred S₁[ Ordinal] means (f,$1) +. a is Element of L;

A1: now :: thesis: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume S₁[O1] ; :: thesis: S₁[ succ O1]
then reconsider fa = (f,O1) +. a as Element of L ;
f . fa = (f,(succ O1)) +. a by Th15;
hence S₁[ succ O1] ; :: thesis: verum

end;

A2: now :: thesis: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) holds
S₁[O1]

let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) implies S₁[O1] )
assume that
A3: ( O1 <> 0 & O1 is limit_ordinal ) and
for O2 being Ordinal st O2 in O1 holds
S₁[O2] ; :: thesis: S₁[O1]
consider Ls being Sequence such that
A4: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H₁(O2) ) ) from ORDINAL2:sch 2();
(f,O1) +. a = "\/" ((rng Ls),L) by A3, A4, Th17;
hence S₁[O1] ; :: thesis: verum

end;

A5: S₁[ 0 ] by Th13;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A5, A1, A2);
hence (f,O) +. a is Element of L ; :: thesis: verum