let i, j be ordinal Element of RAT+ ; :: thesis: i *' j = i *^ j
set ni = numerator i;
set nj = numerator j;
A1: j in omega by ORDINAL1:def 12;
then A2: denominator j = 1 by Def9;
A3: i in omega by ORDINAL1:def 12;
then denominator i = 1 by Def9;
hence i *' j = ((numerator i) *^ (numerator j)) / 1 by A2, ORDINAL2:39
.= (numerator i) *^ (numerator j) by Th40
.= i *^ (numerator j) by A3, Def8
.= i *^ j by A1, Def8 ;
:: thesis: verum