let F be Field; :: thesis: for E being FieldExtension of F
for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in E holds
p splits_in E
let E be FieldExtension of F; :: thesis: for p being non constant Polynomial of F
for q being non zero Polynomial of F st p *' q splits_in E holds
p splits_in E
let p be non constant Polynomial of F; :: thesis: for q being non zero Polynomial of F st p *' q splits_in E holds
p splits_in E
let q be non zero Polynomial of F; :: thesis: ( p *' q splits_in E implies p splits_in E )
assume p *' q splits_in E ; :: thesis: p splits_in E
then consider b being non zero Element of E, s being Ppoly of E such that
A: p *' q = b * s by FIELD_4:def 5;
B: F is Subring of E by FIELD_4:def 1;
then reconsider p1 = p, q1 = q as Polynomial of E by FIELD_4:9;
( p is Element of the carrier of (Polynom-Ring F) & p1 is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
then ( deg p > 0 & deg p = deg p1 ) by RATFUNC1:def 2, FIELD_4:20;
then reconsider p1 = p1 as non constant Polynomial of E by RATFUNC1:def 2;
( q <> 0_. F & 0_. E = 0_. F ) by B, C0SP1:def 3;
then reconsider q1 = q1 as non zero Polynomial of E by UPROOTS:def 5;
p *' q = p1 *' q1 by FIELD_4:17;
then p1 splits_in E by A, FIELD_4:def 5, FIELD_8:11;
then consider a being non zero Element of E, r being Ppoly of E such that
C: p1 = a * r by FIELD_4:def 5;
thus p splits_in E by C, FIELD_4:def 5; :: thesis: verum