let R be Ring; :: thesis: for S being RingExtension of R

for p being Polynomial of R holds p is Polynomial of S

let S be RingExtension of R; :: thesis: for p being Polynomial of R holds p is Polynomial of S

let p be Polynomial of R; :: thesis: p is Polynomial of S

A1: R is Subring of S by Def1;

then A2: the carrier of R c= the carrier of S by C0SP1:def 3;

A3: 0. S = 0. R by A1, C0SP1:def 3;

rng p c= the carrier of R by RELAT_1:def 19;

then rng p c= the carrier of S by A2;

then reconsider p1 = p as sequence of the carrier of S by FUNCT_2:6;

A4: Support p is finite by POLYNOM1:def 5;

hence p is Polynomial of S by A4, POLYNOM1:def 5; :: thesis: verum

for p being Polynomial of R holds p is Polynomial of S

let S be RingExtension of R; :: thesis: for p being Polynomial of R holds p is Polynomial of S

let p be Polynomial of R; :: thesis: p is Polynomial of S

A1: R is Subring of S by Def1;

then A2: the carrier of R c= the carrier of S by C0SP1:def 3;

A3: 0. S = 0. R by A1, C0SP1:def 3;

rng p c= the carrier of R by RELAT_1:def 19;

then rng p c= the carrier of S by A2;

then reconsider p1 = p as sequence of the carrier of S by FUNCT_2:6;

A4: Support p is finite by POLYNOM1:def 5;

now :: thesis: for o being object st o in Support p1 holds

o in Support p

then
Support p1 c= Support p
;o in Support p

let o be object ; :: thesis: ( o in Support p1 implies o in Support p )

assume A5: o in Support p1 ; :: thesis: o in Support p

then reconsider n = o as Element of NAT ;

A6: 0. R <> p . n by A3, A5, POLYNOM1:def 3;

dom p = NAT by FUNCT_2:def 1;

hence o in Support p by A6, POLYNOM1:def 3; :: thesis: verum

end;assume A5: o in Support p1 ; :: thesis: o in Support p

then reconsider n = o as Element of NAT ;

A6: 0. R <> p . n by A3, A5, POLYNOM1:def 3;

dom p = NAT by FUNCT_2:def 1;

hence o in Support p by A6, POLYNOM1:def 3; :: thesis: verum

hence p is Polynomial of S by A4, POLYNOM1:def 5; :: thesis: verum