let F be Field; :: thesis: for E being F -finite FieldExtension of F st E is F -normal holds
ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p
let E be F -finite FieldExtension of F; :: thesis: ( E is F -normal implies ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p )
assume AS: E is F -normal ; :: thesis: ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p
consider T being finite F -algebraic Subset of E such that
A: E == FAdj (F,T) by FIELD_7:37;

per cases ( T is empty or not T is empty ) ;

suppose T is empty ; :: thesis: ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p

then for o being object st o in T holds
o in the carrier of F ;
then T is Subset of the carrier of F by TARSKI:def 3;
then H: FAdj (F,T) == F by FIELD_7:3;
reconsider p = rpoly (1,(0. F)) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg (rpoly (1,(0. F))) = 1 by HURWITZ:27;
then reconsider p = p as linear Element of the carrier of (Polynom-Ring F) by FIELD_5:def 1;
F is SplittingField of p by lemNor1e;
then FAdj (F,T) is SplittingField of p by H, lemNor1d;
then E is SplittingField of p by A, lemNor1d;
hence ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p ; :: thesis: verum

end;

suppose not T is empty ; :: thesis: ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p

then reconsider T = T as non empty finite F -algebraic Subset of E ;
set M = { (MinPoly (a,F)) where a is Element of T : verum } ;
set x = the Element of T;
E: MinPoly ( the Element of T,F) in { (MinPoly (a,F)) where a is Element of T : verum } ;

now :: thesis: for o being object st o in { (MinPoly (a,F)) where a is Element of T : verum } holds
o in the carrier of (Polynom-Ring F)

let o be object ; :: thesis: ( o in { (MinPoly (a,F)) where a is Element of T : verum } implies o in the carrier of (Polynom-Ring F) )
assume o in { (MinPoly (a,F)) where a is Element of T : verum } ; :: thesis: o in the carrier of (Polynom-Ring F)
then consider a being Element of T such that
F: o = MinPoly (a,F) ;
thus o in the carrier of (Polynom-Ring F) by F; :: thesis: verum

end;

then reconsider M = { (MinPoly (a,F)) where a is Element of T : verum } as non empty Subset of the carrier of (Polynom-Ring F) by E, TARSKI:def 3;
defpred S₁[ object , object ] means ex a being Element of T st
( a = $1 & $2 = MinPoly (a,F) );
E1: for a being Element of T ex y being Element of M st S₁[a,y]

proof

let a be Element of T; :: thesis: ex y being Element of M st S₁[a,y]
MinPoly (a,F) in { (MinPoly (a,F)) where a is Element of T : verum } ;
then reconsider y = MinPoly (a,F) as Element of M ;
take y ; :: thesis: S₁[a,y]
thus S₁[a,y] ; :: thesis: verum

end;

consider f being Function of T,M such that
E2: for a being Element of T holds S₁[a,f . a] from FUNCT_2:sch 3(E1);
E3: dom f = T by FUNCT_2:def 1;
rng f = M

proof

E4: now :: thesis: for o being object st o in M holds
o in rng f

let o be object ; :: thesis: ( o in M implies o in rng f )
assume o in M ; :: thesis: o in rng f
then consider a being Element of T such that
E5: o = MinPoly (a,F) ;
S₁[a,f . a] by E2;
hence o in rng f by E5, E3, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for o being object st o in rng f holds
o in M

let o be object ; :: thesis: ( o in rng f implies o in M )
assume o in rng f ; :: thesis: o in M
then consider a being object such that
E4: ( a in dom f & f . a = o ) by FUNCT_1:def 3;
reconsider a = a as Element of T by E4;
S₁[a,o] by E2, E4;
hence o in M ; :: thesis: verum

end;

hence rng f = M by E4, TARSKI:2; :: thesis: verum

end;

then reconsider M = M as non empty finite Subset of the carrier of (Polynom-Ring F) ;
( rng (canFS M) c= M & M c= the carrier of (Polynom-Ring F) ) by FINSEQ_1:def 4;
then ( len (canFS M) = card M & rng (canFS M) c= the carrier of (Polynom-Ring F) ) by FINSEQ_1:93;
then reconsider G = canFS M as non empty FinSequence of the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
reconsider p = Product G as Element of the carrier of (Polynom-Ring F) ;
F: ex i being Element of dom G st G . i = MinPoly ( the Element of T,F)

proof

rng (canFS M) = M by FUNCT_2:def 3;
then MinPoly ( the Element of T,F) in rng (canFS M) ;
then consider i being object such that
H: ( i in dom (canFS M) & (canFS M) . i = MinPoly ( the Element of T,F) ) by FUNCT_1:def 3;
thus ex i being Element of dom G st G . i = MinPoly ( the Element of T,F) by H; :: thesis: verum

end;

not Product G is constant

proof

now :: thesis: for i being Element of dom G holds G . i <> 0_. F

let i be Element of dom G; :: thesis: G . i <> 0_. F
H1: G . i in rng G by FUNCT_1:def 3;
rng (canFS M) c= M by FINSEQ_1:def 4;
then G . i in M by H1;
then consider a being Element of T such that
H2: G . i = MinPoly (a,F) ;
thus G . i <> 0_. F by H2; :: thesis: verum

end;

then H: deg p >= deg (MinPoly ( the Element of T,F)) by F, lemNor1deg;
deg (MinPoly ( the Element of T,F)) > 0 by RING_4:def 4;
hence not Product G is constant by H, RING_4:def 4; :: thesis: verum

end;

then reconsider p = Product G as non constant Element of the carrier of (Polynom-Ring F) ;
D: p splits_in E

proof

deg p > 0 by RING_4:def 4;
then reconsider q = p as non constant Polynomial of F by RATFUNC1:def 2;

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 p is constant or p splits_in E )
let p be Polynomial of F; :: thesis: ( not p = G . i or p is constant or p splits_in E )
assume D1: p = G . i ; :: thesis: ( p is constant or p splits_in E )
( rng G c= M & G . i in rng G ) by FUNCT_1:3, FINSEQ_1:def 4;
then G . i in M ;
then consider a being Element of T such that
D2: G . i = MinPoly (a,F) ;
thus ( p is constant or p splits_in E ) by D1, D2, AS, lemmin; :: thesis: verum

end;

then q splits_in E by lemNor1a;
hence p splits_in E ; :: thesis: verum

end;

now :: thesis: for K being FieldExtension of F st p splits_in K & K is Subfield of E holds
K == E

let K be FieldExtension of F; :: thesis: ( p splits_in K & K is Subfield of E implies K == E )
assume E1: ( p splits_in K & K is Subfield of E ) ; :: thesis: K == E
then E2: ( F is Subfield of K & E is K -extending ) by FIELD_4:7;
then E3: Roots (K,p) = Roots (E,p) by D, E1, FIELD_8:29;
E4: Roots (E,p) = { a where a is Element of E : a is_a_root_of p,E } by FIELD_4:def 4;
T is Subset of K

proof

now :: thesis: for o being object st o in T holds
o in the carrier of K

let o be object ; :: thesis: ( o in T implies o in the carrier of K )
assume o in T ; :: thesis: o in the carrier of K
then reconsider a = o as Element of T ;
rng G = M by FUNCT_2:def 3;
then MinPoly (a,F) in rng G ;
then consider i being object such that
E5: ( i in dom G & G . i = MinPoly (a,F) ) by FUNCT_1:def 3;
Ext_eval ((MinPoly (a,F)),a) = 0. E by FIELD_6:52;
then Ext_eval (p,a) = 0. E by E5, lemNor1b;
then a is_a_root_of p,E by FIELD_4:def 2;
then a in Roots (E,p) by E4;
hence o in the carrier of K by E3; :: thesis: verum

end;

hence T is Subset of K by TARSKI:def 3; :: thesis: verum

end;

then FAdj (F,T) is Subfield of K by E1, E2, FIELD_6:37;
then K is FAdj (F,T) -extending by FIELD_4:7;
then K is E -extending by A, FIELD_12:37;
then E is Subfield of K by FIELD_4:7;
hence K == E by E1, FIELD_7:def 2; :: thesis: verum

end;

then E is SplittingField of p by D, FIELD_8:def 1;
hence ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p ; :: thesis: verum

end;

end;