theorem T4a: :: RING_4:17

for R being Ring
for a, b being Element of R holds (a | R) + (b | R) = (a + b) | R