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
consider r being FinSequence of the carrier of R such that
A3: ( len r = n + 1 & (p *' q) . n = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def 9;
consider r1 being FinSequence of the carrier of S such that
A4: ( len r1 = n + 1 & (p1 *' q2) . n = Sum r1 & ( for k being Element of NAT st k in dom r1 holds
r1 . k = (p1 . (k -' 1)) * (q2 . ((n + 1) -' k)) ) ) by POLYNOM3:def 9;
A5: dom r1 = Seg (len r) by A3, A4, FINSEQ_1:def 3
.= dom r by FINSEQ_1:def 3 ;

now :: thesis: for m being Nat st m in dom r holds
r . m = r1 . m

let m be Nat; :: thesis: ( m in dom r implies r . m = r1 . m )
assume A6: m in dom r ; :: thesis: r . m = r1 . m
( p . (m -' 1) = p1 . (m -' 1) & q . ((n + 1) -' m) = q2 . ((n + 1) -' m) ) by A1;
then A7: [(p1 . (m -' 1)),(q2 . ((n + 1) -' m))] in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2;
thus r . m = (p . (m -' 1)) * (q . ((n + 1) -' m)) by A6, A3
.= ( the multF of S || the carrier of R) . ((p1 . (m -' 1)),(q2 . ((n + 1) -' m))) by A1, A2, C0SP1:def 3
.= (p1 . (m -' 1)) * (q2 . ((n + 1) -' m)) by A7, FUNCT_1:49
.= r1 . m by A6, A5, A4 ; :: thesis: verum

end;

then r = r1 by A5;
hence (p *' q) . n = (p1 *' q2) . n by A4, A3, A2, Th2; :: thesis: verum

end;

hence p *' q = p1 *' q2 ; :: thesis: verum