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