defpred S₁[ natural Ordinal] means a *^ b is natural ;
A1: S₁[ {} ] by ORDINAL2:52;

A2: now

let a be natural Ordinal; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume S₁[a] ; :: thesis: S₁[ succ a]
then reconsider c = a *^ b as natural Ordinal ;
(succ a) *^ b = c +^ b by ORDINAL2:53;
hence S₁[ succ a] ; :: thesis: verum

end;

S₁[a] from ORDINAL2:sch 17(A1, A2);
hence a *^ b is natural ; :: thesis: verum