defpred S₁[ Ordinal] means ( $1 is Ordinal of F₁() implies P₁[$1] );
A4: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A5: ( A <> 0 & A is limit_ordinal ) and
A6: for B being Ordinal st B in A & B is Ordinal of F₁() holds
P₁[B] ; :: thesis: S₁[A]
assume A is Ordinal of F₁() ; :: thesis: P₁[A]
then reconsider a = A as Ordinal of F₁() ;
( {} = 0-element_of F₁() & ( for b being Ordinal of F₁() st b in a holds
P₁[b] ) ) by A6, ORDINAL4:33;
hence P₁[A] by A3, A5; :: thesis: verum

end;

A7: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume that
A8: ( A is Ordinal of F₁() implies P₁[A] ) and
A9: succ A is Ordinal of F₁() ; :: thesis: P₁[ succ A]
( A in succ A & succ A in On F₁() ) by A9, ORDINAL1:6, ORDINAL1:def 9;
then A in On F₁() by ORDINAL1:10;
then reconsider a = A as Ordinal of F₁() by ORDINAL1:def 9;
P₁[ succ a] by A2, A8;
hence P₁[ succ A] ; :: thesis: verum

end;

A10: S₁[ 0 ] by A1, ORDINAL4:33;
for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A10, A7, A4);
hence for a being Ordinal of F₁() holds P₁[a] ; :: thesis: verum