let R be Ring; :: thesis: for S being RingExtension of R
for p, q being Polynomial of R
for p1, q1 being Polynomial of S st p = p1 & q = q1 holds
p + q = p1 + q1
let S be RingExtension of R; :: thesis: for p, q being Polynomial of R
for p1, q1 being Polynomial of S st p = p1 & q = q1 holds
p + q = p1 + q1
let p, q be Polynomial of R; :: thesis: for p1, q1 being Polynomial of S st p = p1 & q = q1 holds
p + q = p1 + q1
let p1, q2 be Polynomial of S; :: thesis: ( p = p1 & q = q2 implies p + q = p1 + q2 )
assume A1: ( p = p1 & q = q2 ) ; :: thesis: p + q = p1 + q2
A2: R is Subring of S by Def1;

now :: thesis: for n being Element of NAT holds (p + q) . n = (p1 + q2) . n

let n be Element of NAT ; :: thesis: (p + q) . n = (p1 + q2) . n
( p . n = p1 . n & q . n = q2 . n ) by A1;
then A3: [(p1 . n),(q2 . n)] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
thus (p + q) . n = (p . n) + (q . n) by NORMSP_1:def 2
.= ( the addF of S || the carrier of R) . ((p1 . n),(q2 . n)) by A1, A2, C0SP1:def 3
.= (p1 . n) + (q2 . n) by A3, FUNCT_1:49
.= (p1 + q2) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence p + q = p1 + q2 ; :: thesis: verum