theorem Th12: :: ALGNUM_1:8
for A, B being Ring
for x1, x2 being Element of A st A is Subring of B holds
(In (x1,B)) + (In (x2,B)) = In ((x1 + x2),B)