let two, i be Element of RAT+ ; :: thesis: ( two = 2 implies i + i = two *' i )
assume A0: two = 2 ; :: 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 A0, Lm13, ARYTM_3:57 ; :: thesis: verum