let F be Field; :: thesis: ex E1 being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) holds p is_with_roots_in E1
set b = the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
set I = the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ;
set KF = KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal );
consider FP being Field such that
X1: ( KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ),FP are_isomorphic & the carrier of FP /\ ( the carrier of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )) \/ the carrier of F) = {} ) by FIELD_5:29;
X: ( [#] F = the carrier of F & [#] FP = the carrier of FP ) ;
X2: F,FP are_disjoint

proof

now :: thesis: not the carrier of F /\ the carrier of FP <> {}

assume A: the carrier of F /\ the carrier of FP <> {} ; :: thesis: contradiction
set x = the Element of the carrier of F /\ the carrier of FP;
B: ( the Element of the carrier of F /\ the carrier of FP in the carrier of F & the Element of the carrier of F /\ the carrier of FP in the carrier of FP ) by A, XBOOLE_0:def 4;
then the Element of the carrier of F /\ the carrier of FP in the carrier of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )) \/ the carrier of F by XBOOLE_0:def 3;
hence contradiction by B, X1, XBOOLE_0:def 4; :: thesis: verum

end;

hence F,FP are_disjoint by X, FIELD_2:def 1; :: thesis: verum

end;

consider phi being Function of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )),FP such that
X3: phi is isomorphism by X1;
set h = phi * (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))));
reconsider h = phi * (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) as Function of F,FP ;
X4: ( h is linear & h is one-to-one ) by X3, RINGCAT1:1;
then reconsider FP = FP as F -monomorphic Field by RING_3:def 3;
reconsider h = h as Monomorphism of F,FP by X4;
reconsider E = embField h as Field by X2, FIELD_2:12;
emb_iso h is onto by X2, FIELD_2:15;
then reconsider embisoh = (emb_iso h) " as Function of FP,E by FUNCT_2:25;
( emb_iso h is additive & emb_iso h is multiplicative ) by X2, FIELD_2:13, FIELD_2:14;
then Y: ( emb_iso h is linear & emb_iso h is one-to-one & emb_iso h is onto ) by X2, FIELD_2:15;
then reconsider FP = FP as E -isomorphic Field by RING_3:def 4;
reconsider embisoh = embisoh as Isomorphism of FP,E by Y, RING_3:73;
set iso = embisoh * phi;
reconsider iso = embisoh * phi as Function of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )),E ;
X5: iso is RingHomomorphism by X3, RINGCAT1:1;
then reconsider E = E as KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ) -homomorphic Field by RING_2:def 4;
reconsider iso = iso as Homomorphism of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )),E by X5;
F is Subfield of E by FIELD_2:17;
then reconsider E = E as FieldExtension of F by FIELD_4:7;
take E ; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds p is_with_roots_in E

now :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds p is_with_roots_in E

let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: p is_with_roots_in E
set u = KrRoot ( the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ,( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)) . p));
set n = card (nonConstantPolys F);
KrRoot ( the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ,( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)) . p)) is_a_root_of (PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p by Kr1;
then B: eval (((PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p)),(iso . (KrRoot ( the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ,( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)) . p))))) = 0. E by FIELD_1:33, POLYNOM5:def 7;
reconsider a = iso . (KrRoot ( the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal ,( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)) . p))) as Element of E ;
(PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p) = p

proof

set g = (PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p);
A: for a being Element of F holds iso . ((emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) . a) = a

proof

let a be Element of F; :: thesis: iso . ((emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) . a) = a
a | ((card (nonConstantPolys F)),F) is Element of (Polynom-Ring ((card (nonConstantPolys F)),F)) by POLYNOM1:def 11;
then reconsider v = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )),(a | ((card (nonConstantPolys F)),F))) as Element of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )) by RING_1:12;
dom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) = the carrier of F by FUNCT_2:def 1;
then C: h . a = phi . ((emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) . a) by FUNCT_1:13
.= phi . v by TH39 ;
the carrier of (embField h) = carr h by FIELD_2:def 7
.= (([#] FP) \ (rng h)) \/ ([#] F) by FIELD_2:def 2
.= ( the carrier of FP \ (rng h)) \/ the carrier of F ;
then reconsider a1 = a as Element of (embField h) by XBOOLE_0:def 3;
a in F ;
then D: (emb_iso h) . a1 = phi . v by C, FIELD_2:def 8;
A1: dom phi = the carrier of (KroneckerField (F, the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )) by FUNCT_2:def 1;
A3: dom (emb_iso h) = the carrier of E by FUNCT_2:def 1;
thus iso . ((emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) . a) = (embisoh * phi) . v by TH39
.= ((emb_iso h) ") . (phi . v) by A1, FUNCT_1:13
.= a by D, A3, FUNCT_1:34 ; :: thesis: verum

end;

now :: thesis: for x being object st x in NAT holds
((PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p)) . x = p . x

let x be object ; :: thesis: ( x in NAT implies ((PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p)) . x = p . x )
assume x in NAT ; :: thesis: ((PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p)) . x = p . x
then reconsider i = x as Element of NAT ;
((PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p)) . i = iso . (((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p) . i) by FIELD_1:def 2
.= iso . (Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)), the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal )),((p . i) | ((card (nonConstantPolys F)),F)))) by TH40
.= iso . ((emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)))) . (p . i)) by TH39 ;
hence ((PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p)) . x = p . x by A; :: thesis: verum

end;

hence (PolyHom iso) . ((PolyHom (emb (F, the maxIdeal of (nonConstantPolys ( the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)),F)) -Ideal , the bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))))) . p) = p ; :: thesis: verum

end;

then Ext_eval (p,a) = 0. E by B, FIELD_4:26;
hence p is_with_roots_in E by FIELD_4:def 3, FIELD_4:def 2; :: thesis: verum

end;

hence for p being non constant Element of the carrier of (Polynom-Ring F) holds p is_with_roots_in E ; :: thesis: verum