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) *^ 1) +^ (1 *^ (numerator j))) / 1 by A2, ORDINAL2:39
.= ((numerator i) +^ (1 *^ (numerator j))) / 1 by ORDINAL2:39
.= ((numerator i) +^ (numerator j)) / 1 by ORDINAL2:39
.= (numerator i) +^ (numerator j) by Th40
.= i +^ (numerator j) by A3, Def8
.= i +^ j by A1, Def8 ;
:: thesis: verum