defpred S₁[ Nat] means for a being Ordinal
for n being non zero Nat st $1 = n holds
P₁[n *^ (exp (omega,a))];
A4: S₁[1]

proof

let a be Ordinal; :: thesis: for n being non zero Nat st 1 = n holds
P₁[n *^ (exp (omega,a))]
let n be non zero Nat; :: thesis: ( 1 = n implies P₁[n *^ (exp (omega,a))] )
assume 1 = n ; :: thesis: P₁[n *^ (exp (omega,a))]
then n *^ (exp (omega,a)) = exp (omega,a) by ORDINAL2:39;
hence P₁[n *^ (exp (omega,a))] by A1; :: thesis: verum

end;

A5: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let a be Ordinal; :: thesis: for n being non zero Nat st k + 1 = n holds
P₁[n *^ (exp (omega,a))]
let n be non zero Nat; :: thesis: ( k + 1 = n implies P₁[n *^ (exp (omega,a))] )
assume A7: k + 1 = n ; :: thesis: P₁[n *^ (exp (omega,a))]
P₁[k *^ (exp (omega,a))] by A6;
hence P₁[n *^ (exp (omega,a))] by A2, A7; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A4, A5);
then A8: for a being Ordinal
for n being non zero Nat holds P₁[n *^ (exp (omega,a))] ;
for a being non empty Ordinal holds P₁[a] from ORDINAL7:sch 1(A8, A3);
hence for a being non empty Ordinal holds P₁[a] ; :: thesis: verum