defpred S₁[ Ordinal] means f,$1 -. a is Element of L;
A1: S₁[ {} ] by Th17;

A2: now

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 Th19;
hence S₁[ succ O1] ; :: thesis: verum

end;

deffunc H₁( Ordinal) -> set = f,$1 -. a;

A3: now

let O1 be Ordinal; :: thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) implies S₁[O1] )
assume A4: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) ) ; :: thesis: S₁[O1]
consider Ls being T-Sequence such that
A5: ( 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 A4, A5, Th21;
hence S₁[O1] ; :: thesis: verum

end;

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