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