let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
Roots (S,p) = Roots q
let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) st p = q holds
Roots (S,p) = Roots q
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for q being Element of the carrier of (Polynom-Ring S) st p = q holds
Roots (S,p) = Roots q
let q be Element of the carrier of (Polynom-Ring S); :: thesis: ( p = q implies Roots (S,p) = Roots q )
I: Roots (S,p) = { a where a is Element of S : a is_a_root_of p,S } by FIELD_4:def 4;
assume AS: p = q ; :: thesis: Roots (S,p) = Roots q

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

let o be object ; :: thesis: ( o in Roots q implies o in Roots (S,p) )
assume A0: o in Roots q ; :: thesis: o in Roots (S,p)
then reconsider a = o as Element of S ;
a is_a_root_of q by A0, POLYNOM5:def 10;
then 0. S = eval (q,a) by POLYNOM5:def 7
.= Ext_eval (p,a) by AS, FIELD_4:26 ;
then a is_a_root_of p,S by FIELD_4:def 2;
hence o in Roots (S,p) by I; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in Roots (S,p) implies o in Roots q )
assume o in Roots (S,p) ; :: thesis: o in Roots q
then consider a being Element of S such that
A1: ( o = a & a is_a_root_of p,S ) by I;
0. S = Ext_eval (p,a) by A1, FIELD_4:def 2
.= eval (q,a) by AS, FIELD_4:26 ;
then a is_a_root_of q by POLYNOM5:def 7;
hence o in Roots q by A1, POLYNOM5:def 10; :: thesis: verum

end;

hence Roots (S,p) = Roots q by A, TARSKI:2; :: thesis: verum