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:56;
then A6: RED ((denominator x9) *^ (denominator y9)),(((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9))) = one by ARYTM_3:29;
((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9)) = ((numerator x9) *^ one ) +^ (numerator y9) by A2, A4, ORDINAL2:56
.= (numerator x9) +^ (numerator y9) by ORDINAL2:56
.= 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:29
.= x9 + y9 by A6, ARYTM_3:def 10 ;
:: thesis: verum