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