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;

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)

hence
Roots p c= Roots (S,p)
; :: thesis: verumo 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;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