let F be Field; for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b2 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) = Roots (U,p) )
let p be non constant Element of the carrier of (Polynom-Ring F); for U being FieldExtension of F
for E being b1 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) = Roots (U,p) )
let U be FieldExtension of F; for E being U -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) = Roots (U,p) )
let E be U -extending FieldExtension of F; ( p splits_in E implies ( p splits_in U iff Roots (E,p) = Roots (U,p) ) )
assume AS:
p splits_in E
; ( p splits_in U iff Roots (E,p) = Roots (U,p) )
now ( p splits_in U implies Roots (E,p) = Roots (U,p) )assume
p splits_in U
;
Roots (E,p) = Roots (U,p)then B:
Roots (
E,
p)
c= Roots (
U,
p)
by AS, lemma3;
Roots (
U,
p)
c= Roots (
E,
p)
by lemma7;
hence
Roots (
E,
p)
= Roots (
U,
p)
by B, XBOOLE_0:def 10;
verum end;
hence
( p splits_in U iff Roots (E,p) = Roots (U,p) )
by AS, lemma3; verum