let a, b be natural Ordinal; :: thesis: a *^ b = b *^ a
defpred S1[ natural Ordinal] means a *^ $1 = $1 *^ a;
A1: now
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
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, Th33
.= (a *^ b) +^ (succ (a +^ b)) by ORDINAL2:28
.= succ ((a *^ b) +^ (a +^ b)) by ORDINAL2:28
.= succ (((a *^ b) +^ b) +^ a) by Th33
.= 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[ {} ] ;
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[ {} ] ;
thus S1[b] from ORDINAL2:sch 17(A6, A1); :: thesis: verum