theorem Th13: :: RING_1:13

for R being non empty right_complementable distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))