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] )
defpred S2[ natural Ordinal] means $1 *^ (succ b) = ($1 *^ b) +^ $1;
assume A2: S1[b] ; :: thesis: S1[ succ b]
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 a) *^ (succ b) = (a *^ (succ b)) +^ (succ b) by ORDINAL2:36
.= (a *^ b) +^ (a +^ (succ b)) by A4, Th30
.= (a *^ b) +^ (succ (a +^ b)) by ORDINAL2:28
.= succ ((a *^ b) +^ (a +^ b)) by ORDINAL2:28
.= succ (((a *^ b) +^ b) +^ a) by Th30
.= succ (((succ a) *^ b) +^ a) by ORDINAL2:36
.= ((succ a) *^ b) +^ (succ a) by ORDINAL2:28 ;
hence S2[ succ a] ; :: thesis: verum
end;
{} *^ (succ b) = {} by ORDINAL2:35
.= {} +^ {} by ORDINAL2:27
.= ({} *^ b) +^ {} by ORDINAL2:35 ;
then A5: S2[ 0 ] ;
S2[a] from ORDINAL2:sch 17(A5, A3);
hence S1[ succ b] by A2, ORDINAL2:36; :: thesis: verum
end;
a *^ {} = {} by ORDINAL2:38
.= {} *^ a by ORDINAL2:35 ;
then A6: S1[ 0 ] ;
thus S1[b] from ORDINAL2:sch 17(A6, A1); :: thesis: verum