let i, j be Element of omega ; :: thesis: for x', y' being Element of RAT+ st i = x' & j = y' holds
i +^ j = x' + y'
let x', y' be Element of RAT+ ; :: thesis: ( i = x' & j = y' implies i +^ j = x' + y' )
set a = (denominator x') *^ (denominator y');
set b = ((numerator x') *^ (denominator y')) +^ ((numerator y') *^ (denominator x'));
assume A1: i = x' ; :: thesis: ( not j = y' or i +^ j = x' + y' )
then A2: denominator x' = one by ARYTM_3:def 9;
assume A3: j = y' ; :: thesis: i +^ j = x' + y'
then A4: denominator y' = one by ARYTM_3:def 9;
then A5: (denominator x') *^ (denominator y') = one by A2, ORDINAL2:56;
then A6: RED ((denominator x') *^ (denominator y')),(((numerator x') *^ (denominator y')) +^ ((numerator y') *^ (denominator x'))) = one by ARYTM_3:29;
((numerator x') *^ (denominator y')) +^ ((numerator y') *^ (denominator x')) = ((numerator x') *^ one ) +^ (numerator y') by A2, A4, ORDINAL2:56
.= (numerator x') +^ (numerator y') by ORDINAL2:56
.= i +^ (numerator y') by A1, ARYTM_3:def 8
.= i +^ j by A3, ARYTM_3:def 8 ;
hence i +^ j = RED (((numerator x') *^ (denominator y')) +^ ((numerator y') *^ (denominator x'))),((denominator x') *^ (denominator y')) by A5, ARYTM_3:29
.= x' + y' by A6, ARYTM_3:def 10 ;
:: thesis: verum