let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for U being FieldExtension of E st p splits_in E holds
p splits_in U
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: for E being FieldExtension of F
for U being FieldExtension of E st p splits_in E holds
p splits_in U
let E be FieldExtension of F; :: thesis: for U being FieldExtension of E st p splits_in E holds
p splits_in U
let U be FieldExtension of E; :: thesis: ( p splits_in E implies p splits_in U )
assume p splits_in E ; :: thesis: p splits_in U
then consider a being non zero Element of E, q being Ppoly of E such that
A: p = a * q by FIELD_4:def 5;
B: E is Subfield of U by FIELD_4:7;
then the carrier of E c= the carrier of U by EC_PF_1:def 1;
then reconsider b = a as Element of U ;
( a <> 0. E & 0. U = 0. E ) by B, EC_PF_1:def 1;
then reconsider b = b as non zero Element of U by STRUCT_0:def 12;
reconsider r = q as Ppoly of U by lemmapp;
C: b | U = a | E by FIELD_6:23;
b * r = (b | U) *' r by poly1
.= (a | E) *' q by C, FIELD_4:17
.= a * q by poly1 ;
hence p splits_in U by A, FIELD_4:def 5; :: thesis: verum