let a, b be natural Ordinal; :: thesis: a +^ b = b +^ a
defpred S₁[ natural Ordinal] means a +^ $1 = $1 +^ a;

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

let b be natural Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume A2: S₁[b] ; :: thesis: S₁[ succ b]
defpred S₂[ natural Ordinal] means (succ b) +^ $1 = succ (b +^ $1);

A3: 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 A4: S₂[a] ; :: thesis: S₂[ succ a]
(succ b) +^ (succ a) = succ ((succ b) +^ a) by ORDINAL2:28
.= succ (b +^ (succ a)) by A4, ORDINAL2:28 ;
hence S₂[ succ a] ; :: thesis: verum

end;

(succ b) +^ {} = succ b by ORDINAL2:27
.= succ (b +^ {}) by ORDINAL2:27 ;
then A5: S₂[ 0 ] ;
S₂[a] from ORDINAL2:sch 17(A5, A3);
hence S₁[ succ b] by A2, ORDINAL2:28; :: thesis: verum

end;

a +^ {} = a by ORDINAL2:27
.= {} +^ a by ORDINAL2:30 ;
then A6: S₁[ 0 ] ;
thus S₁[b] from ORDINAL2:sch 17(A6, A1); :: thesis: verum