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;

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

hence
p *' q = p1 *' q2
; :: thesis: verumlet 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 ;

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

end;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

then
r = r1
by A5;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;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

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