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

A2: now

let b be natural Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume A3: S₁[b] ; :: thesis: S₁[ succ b]
defpred S₂[ natural Ordinal] means (succ b) +^ $1 = succ (b +^ $1);
(succ b) +^ {} = succ b by ORDINAL2:44
.= succ (b +^ {} ) by ORDINAL2:44 ;
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 b) +^ (succ a) = succ ((succ b) +^ a) by ORDINAL2:45
.= succ (b +^ (succ a)) by A6, ORDINAL2:45 ;
hence S₂[ succ a] ; :: thesis: verum

end;

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

end;

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