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

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