let F be Field; :: thesis: for E being FieldExtension of F
for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being non constant Polynomial of F st q = Product G holds
( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) )
let E be FieldExtension of F; :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F)
for q being non constant Polynomial of F st q = Product G holds
( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) )
let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: for q being non constant Polynomial of F st q = Product G holds
( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) )
let q be non constant Polynomial of F; :: thesis: ( q = Product G implies ( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) ) )
assume AS: q = Product G ; :: thesis: ( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) )
J: ( the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring E) & q in the carrier of (Polynom-Ring F) ) by FIELD_4:10, POLYNOM3:def 10;
then reconsider q1 = q as Polynomial of E by POLYNOM3:def 10;
H: ( q is Element of the carrier of (Polynom-Ring F) & q1 is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
deg q > 0 by RATFUNC1:def 2;
then deg q1 > 0 by H, FIELD_4:20;
then reconsider q1 = q1 as non constant Polynomial of E by RATFUNC1:def 2;
rng G c= the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
then rng G c= the carrier of (Polynom-Ring E) by J;
then reconsider G1 = G as non empty FinSequence of the carrier of (Polynom-Ring E) by FINSEQ_1:def 4;
Polynom-Ring F is Subring of Polynom-Ring E by FIELD_4:def 1;
then B: Product G1 = Product G by Eprod;

A: now :: thesis: ( q splits_in E implies for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) )

assume q splits_in E ; :: thesis: for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E )
then consider a being non zero Element of E, q2 being Ppoly of E such that
A3: q = a * q2 by FIELD_4:def 5;
A1: q1 splits_in E by A3, FIELD_4:def 5;

now :: thesis: for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E )

let i be Element of dom G; :: thesis: for p being Polynomial of F holds
( not p = G . i or b₃ is constant or b₃ splits_in E )
let p be Polynomial of F; :: thesis: ( not p = G . i or b₂ is constant or b₂ splits_in E )
assume A2: p = G . i ; :: thesis: ( b₂ is constant or b₂ splits_in E )
reconsider p1 = p as Polynomial of E by FIELD_4:8;
H: ( p is Element of the carrier of (Polynom-Ring F) & p1 is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;

per cases ( p1 is constant or p1 splits_in E ) by B, A1, A2, AS, lemNor1ah;

suppose p1 is constant ; :: thesis: ( b₂ is constant or b₂ splits_in E )

then deg p1 <= 0 by RATFUNC1:def 2;
then deg p <= 0 by H, FIELD_4:20;
hence ( p is constant or p splits_in E ) by RATFUNC1:def 2; :: thesis: verum

end;

suppose p1 splits_in E ; :: thesis: ( b₂ is constant or b₂ splits_in E )

then consider b being non zero Element of E, p2 being Ppoly of E such that
A4: p1 = b * p2 by FIELD_4:def 5;
thus ( p is constant or p splits_in E ) by A4, FIELD_4:def 5; :: thesis: verum

end;

end;

end;

hence for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) ; :: thesis: verum

end;

now :: thesis: ( ( for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) ) implies q splits_in E )

assume A1: for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) ; :: thesis: q splits_in E

now :: thesis: for i being Element of dom G1
for p being Polynomial of E holds
( not p = G1 . i or p is constant or p splits_in E )

let i be Element of dom G1; :: thesis: for p being Polynomial of E holds
( not p = G1 . i or b₃ is constant or b₃ splits_in E )
let p be Polynomial of E; :: thesis: ( not p = G1 . i or b₂ is constant or b₂ splits_in E )
assume A2: p = G1 . i ; :: thesis: ( b₂ is constant or b₂ splits_in E )
then p = G /. i by PARTFUN1:def 6;
then p is Element of the carrier of (Polynom-Ring F) ;
then reconsider p1 = p as Polynomial of F ;
H: ( p1 is Element of the carrier of (Polynom-Ring F) & p is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;

per cases ( p1 is constant or p1 splits_in E ) by A1, A2;

suppose p1 is constant ; :: thesis: ( b₂ is constant or b₂ splits_in E )

then deg p1 <= 0 by RATFUNC1:def 2;
then deg p <= 0 by H, FIELD_4:20;
hence ( p is constant or p splits_in E ) by RATFUNC1:def 2; :: thesis: verum

end;

suppose p1 splits_in E ; :: thesis: ( b₂ is constant or b₂ splits_in E )

then consider b being non zero Element of E, p2 being Ppoly of E such that
A4: p1 = b * p2 by FIELD_4:def 5;
thus ( p is constant or p splits_in E ) by A4, FIELD_4:def 5; :: thesis: verum

end;

end;

end;

then q1 splits_in E by B, AS, lemNor1ah;
then consider a being non zero Element of E, q2 being Ppoly of E such that
A3: q1 = a * q2 by FIELD_4:def 5;
thus q splits_in E by A3, FIELD_4:def 5; :: thesis: verum

end;

hence ( q splits_in E iff for i being Element of dom G
for p being Polynomial of F holds
( not p = G . i or p is constant or p splits_in E ) ) by A; :: thesis: verum