let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
Roots (K,p) = Roots (K,q)
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
Roots (K,p) = Roots (K,q)
let K be E -extending FieldExtension of F; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
Roots (K,p) = Roots (K,q)
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of the carrier of (Polynom-Ring E) st p = q holds
Roots (K,p) = Roots (K,q)
let q be Element of the carrier of (Polynom-Ring E); :: thesis: ( p = q implies Roots (K,p) = Roots (K,q) )
H: ( Roots (K,p) = { a where a is Element of K : a is_a_root_of p,K } & Roots (K,q) = { a where a is Element of K : a is_a_root_of q,K } ) by FIELD_4:def 4;
assume AS: p = q ; :: thesis: Roots (K,p) = Roots (K,q)

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

let o be object ; :: thesis: ( o in Roots (K,p) implies o in Roots (K,q) )
assume o in Roots (K,p) ; :: thesis: o in Roots (K,q)
then consider a being Element of K such that
A: ( o = a & a is_a_root_of p,K ) by H;
Ext_eval (q,a) = Ext_eval (p,a) by AS, FIELD_8:6
.= 0. K by A, FIELD_4:def 2 ;
then a is_a_root_of q,K by FIELD_4:def 2;
hence o in Roots (K,q) by A, H; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in Roots (K,q) implies o in Roots (K,p) )
assume o in Roots (K,q) ; :: thesis: o in Roots (K,p)
then consider a being Element of K such that
B: ( o = a & a is_a_root_of q,K ) by H;
Ext_eval (p,a) = Ext_eval (q,a) by AS, FIELD_8:6
.= 0. K by B, FIELD_4:def 2 ;
then a is_a_root_of p,K by FIELD_4:def 2;
hence o in Roots (K,p) by B, H; :: thesis: verum

end;

hence Roots (K,p) = Roots (K,q) by Z, TARSKI:2; :: thesis: verum