theorem Th17: :: FIELD_6:15

for S being Ring
for R being Subring of S
for x, y being Element of S
for x1, y1 being Element of R st x = x1 & y = y1 holds
x + y = x1 + y1