let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= Roots (S,p)
let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= Roots (S,p)
let p be Element of the carrier of (Polynom-Ring R); :: thesis: Roots p c= Roots (S,p)
A1: R is Subring of S by Def1;
then A2: the carrier of R c= the carrier of S by C0SP1:def 3;

now :: thesis: for o being object st o in Roots p holds
o in Roots (S,p)

let o be object ; :: thesis: ( o in Roots p implies o in Roots (S,p) )
assume A3: o in Roots p ; :: thesis: o in Roots (S,p)
then reconsider a = o as Element of R ;
A4: a is_a_root_of p by A3, POLYNOM5:def 10;
reconsider b = a as Element of S by A2;
Ext_eval (p,b) = eval (p,a) by Th14
.= 0. R by A4, POLYNOM5:def 7
.= 0. S by A1, C0SP1:def 3 ;
then b is_a_root_of p,S ;
hence o in Roots (S,p) ; :: thesis: verum

end;

hence Roots p c= Roots (S,p) ; :: thesis: verum