let i be Element of RAT+ ; :: thesis: i + i = two *' i
thus i + i = (one *' i) + i by ARYTM_3:59
.= (one *' i) + (one *' i) by ARYTM_3:59
.= two *' i by Lm13, ARYTM_3:63 ; :: thesis: verum