defpred S1[ natural Ordinal] means a *^ b is natural ;
A1: now :: thesis: for a being natural Ordinal st S1[a] holds
S1[ succ a]
let a be natural Ordinal; :: thesis: ( S1[a] implies S1[ succ a] )
assume S1[a] ; :: thesis: S1[ succ a]
then reconsider c = a *^ b as natural Ordinal ;
(succ a) *^ b = c +^ b by ORDINAL2:36;
hence S1[ succ a] ; :: thesis: verum
end;
A2: S1[ 0 ] by ORDINAL2:35;
S1[a] from ORDINAL2:sch 17(A2, A1);
hence a *^ b is natural ; :: thesis: verum