let S be Ring; :: thesis: for R being Subring of S
for p being Polynomial of R holds p is Polynomial of S
let R be Subring of S; :: 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
A2: the carrier of R c= the carrier of S by C0SP1:def 3;
A3: 0. S = 0. R by 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

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;

then Support p1 c= Support p ;
hence p is Polynomial of S by A4, POLYNOM1:def 5; :: thesis: verum