let a, b be natural Ordinal; :: thesis: a +^ b = b +^ a
defpred S1[ natural Ordinal] means a +^ $1 = $1 +^ a;
A1: now :: thesis: for b being natural Ordinal st S1[b] holds
S1[ succ b]
let b be natural Ordinal; :: thesis: ( S1[b] implies S1[ succ b] )
assume A2: S1[b] ; :: thesis: S1[ succ b]
defpred S2[ natural Ordinal] means (succ b) +^ $1 = succ (b +^ $1);
A3: now :: thesis: for a being natural Ordinal st S2[a] holds
S2[ succ a]
let a be natural Ordinal; :: thesis: ( S2[a] implies S2[ succ a] )
assume A4: S2[a] ; :: thesis: S2[ succ a]
(succ b) +^ (succ a) = succ ((succ b) +^ a) by ORDINAL2:28
.= succ (b +^ (succ a)) by A4, ORDINAL2:28 ;
hence S2[ succ a] ; :: thesis: verum
end;
(succ b) +^ {} = succ b by ORDINAL2:27
.= succ (b +^ {}) by ORDINAL2:27 ;
then A5: S2[ 0 ] ;
S2[a] from ORDINAL2:sch 17(A5, A3);
hence S1[ succ b] by A2, ORDINAL2:28; :: thesis: verum
end;
a +^ {} = a by ORDINAL2:27
.= {} +^ a by ORDINAL2:30 ;
then A6: S1[ 0 ] ;
thus S1[b] from ORDINAL2:sch 17(A6, A1); :: thesis: verum