let F be Field; for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for U being b2 -extending FieldExtension of F holds Roots (E,p) c= Roots (U,p)
let p be Element of the carrier of (Polynom-Ring F); for E being FieldExtension of F
for U being b1 -extending FieldExtension of F holds Roots (E,p) c= Roots (U,p)
let E be FieldExtension of F; for U being E -extending FieldExtension of F holds Roots (E,p) c= Roots (U,p)
let U be E -extending FieldExtension of F; Roots (E,p) c= Roots (U,p)
E is Subfield of U
by FIELD_4:7;
then H:
( the carrier of E c= the carrier of U & 0. E = 0. U )
by EC_PF_1:def 1;
now for o being object st o in Roots (E,p) holds
o in Roots (U,p)let o be
object ;
( o in Roots (E,p) implies o in Roots (U,p) )assume
o in Roots (
E,
p)
;
o in Roots (U,p)then
o in { a where a is Element of E : a is_a_root_of p,E }
by FIELD_4:def 4;
then consider a being
Element of
E such that A:
(
o = a &
a is_a_root_of p,
E )
;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider p1 =
p as
Element of the
carrier of
(Polynom-Ring E) ;
reconsider U1 =
U as
FieldExtension of
E ;
reconsider b =
a as
Element of
U by H;
Ext_eval (
p,
b) =
Ext_eval (
p,
a)
by FIELD_7:14
.=
0. U
by H, A, FIELD_4:def 2
;
then
b is_a_root_of p,
U
by FIELD_4:def 2;
then
a in { a where a is Element of U : a is_a_root_of p,U }
;
hence
o in Roots (
U,
p)
by A, FIELD_4:def 4;
verum end;
hence
Roots (E,p) c= Roots (U,p)
; verum