theorem prl3: :: RING_5:2

for R being Ring
for a being Element of R holds 2 '*' a = a + a