defpred S₁[ natural Ordinal] means a *^ b is natural ;

A1: now :: thesis: for a being natural Ordinal st S₁[a] holds
S₁[ succ a]

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

end;

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