let a, b be natural Ordinal; :: thesis: a *^ b = b *^ a
defpred S₁[ natural Ordinal] means a *^ $1 = $1 *^ a;
a *^ {} = {} by ORDINAL2:55
.= {} *^ a by ORDINAL2:52 ;
then A1: S₁[ {} ] ;

A2: now

let b be natural Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
defpred S₂[ natural Ordinal] means $1 *^ (succ b) = ($1 *^ b) +^ $1;
assume A3: S₁[b] ; :: thesis: S₁[ succ b]
{} *^ (succ b) = {} by ORDINAL2:52
.= {} +^ {} by ORDINAL2:44
.= ({} *^ b) +^ {} by ORDINAL2:52 ;
then A4: S₂[ {} ] ;

A5: now

let a be natural Ordinal; :: thesis: ( S₂[a] implies S₂[ succ a] )
assume A6: S₂[a] ; :: thesis: S₂[ succ a]
(succ a) *^ (succ b) = (a *^ (succ b)) +^ (succ b) by ORDINAL2:53
.= (a *^ b) +^ (a +^ (succ b)) by A6, Th33
.= (a *^ b) +^ (succ (a +^ b)) by ORDINAL2:45
.= succ ((a *^ b) +^ (a +^ b)) by ORDINAL2:45
.= succ (((a *^ b) +^ b) +^ a) by Th33
.= succ (((succ a) *^ b) +^ a) by ORDINAL2:53
.= ((succ a) *^ b) +^ (succ a) by ORDINAL2:45 ;
hence S₂[ succ a] ; :: thesis: verum

end;

S₂[a] from ORDINAL2:sch 17(A4, A5);
hence S₁[ succ b] by A3, ORDINAL2:53; :: thesis: verum

end;

thus S₁[b] from ORDINAL2:sch 17(A1, A2); :: thesis: verum