defpred S₁[ Ordinal] means ( $1 is natural implies P₁[$1] );

A3: now :: thesis: for A being Ordinal st S₁[A] holds
S₁[ succ A]

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume A4: S₁[A] ; :: thesis: S₁[ succ A]

now :: thesis: ( succ A is natural implies S₁[ succ A] )

assume succ A is natural ; :: thesis: S₁[ succ A]
then A5: succ A in omega ;
A in succ A by ORDINAL1:6;
then A is Element of omega by A5, ORDINAL1:10;
hence S₁[ succ A] by A2, A4; :: thesis: verum

end;

hence S₁[ succ A] ; :: thesis: verum

end;

A6: now :: thesis: 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]

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 A7: A <> 0 ; :: thesis: ( A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
0 c= A ;
then 0 c< A by A7;
then A8: 0 in A by ORDINAL1:11;
A9: not A in A ;
assume A is limit_ordinal ; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
then omega c= A by A8, ORDINAL1:def 11;
then not A in omega by A9;
hence ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] ) by ORDINAL1:def 12; :: thesis: verum

end;

A10: S₁[ 0 ] by A1;
for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A10, A3, A6);
hence P₁[F₁()] ; :: thesis: verum