let A, B be Ring; :: thesis: for x, y being Element of B
for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds
x + y = x1 + y1
let x, y be Element of B; :: thesis: for x1, y1 being Element of A st A is Subring of B & x = x1 & y = y1 holds
x + y = x1 + y1
let x1, y1 be Element of A; :: thesis: ( A is Subring of B & x = x1 & y = y1 implies x + y = x1 + y1 )
assume A is Subring of B ; :: thesis: ( not x = x1 or not y = y1 or x + y = x1 + y1 )
then the addF of A = the addF of B || the carrier of A by C0SP1:def 3;
hence ( not x = x1 or not y = y1 or x + y = x1 + y1 ) by FUNCT_1:49, ZFMISC_1:87; :: thesis: verum