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) *^ 1) +^ (1 *^ (numerator j))) / 1 by ORDINAL2:56
.= ((numerator i) +^ (1 *^ (numerator j))) / 1 by ORDINAL2:56
.= ((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