let F be Field; :: thesis:
let p1 be Element of the carrier of (Polynom-Ring F); :: thesis:

now :: thesis:

assume ( p1 is irreducible & p1 is monic ) ; :: thesis:
then reconsider p = p1 as monic irreducible Element of the carrier of (Polynom-Ring F) ;
set KF = KroneckerField (F,p);
set u = KrRoot p;
consider FP being Field such that
X1: ( KroneckerField (F,p),FP are_isomorphic & the carrier of FP /\ ( the carrier of (KroneckerField (F,p)) \/ 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:

assume A: the carrier of F /\ the carrier of FP <> {} ; :: thesis:
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,p)) \/ the carrier of F by XBOOLE_0:def 3;
hence contradiction by B, X1, XBOOLE_0:def 4; :: thesis:

end;

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

end;

consider phi being Function of (KroneckerField (F,p)),FP such that
X3: phi is isomorphism by X1;
reconsider KroneckerIsop = (KroneckerIso p) " as Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) by RING_3:73;
set h = phi * (emb p);
reconsider h = phi * (emb p) 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 & emb_iso h is unity-preserving ) 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,p)),E ;
X5: iso is RingHomomorphism by X3, RINGCAT1:1;
then reconsider E = E as KroneckerField (F,p) -homomorphic Field by RING_2:def 4;
reconsider iso = iso as Homomorphism of (KroneckerField (F,p)),E by X5;
KrRoot p is_a_root_of emb (p,p) by FIELD_1:42;
then Z: eval (((PolyHom iso) . (emb (p,p))),(iso . (KrRoot p))) = 0. E by FIELD_1:33, POLYNOM5:def 7;
F is Subfield of E by FIELD_2:17;
then reconsider E = E as FieldExtension of F by FIELD_4:7;
take E = E; :: thesis:
reconsider a = iso . (KrRoot p) as Element of E ;
(PolyHom iso) . (emb (p,p)) = p

proof

set g = (PolyHom iso) . (emb (p,p));
A: for a being Element of F holds iso . ((emb p) . a) = a

proof

let a be Element of F; :: thesis:
reconsider b = a | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider v = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),b) as Element of (KroneckerField (F,p)) by RING_1:12;
dom (emb p) = the carrier of F by FUNCT_2:def 1;
then C: h . a = phi . ((emb p) . a) by FUNCT_1:13
.= phi . v by FIELD_1:39 ;
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,p)) by FUNCT_2:def 1;
A3: dom (emb_iso h) = the carrier of E by FUNCT_2:def 1;
thus iso . ((emb p) . a) = (embisoh * phi) . v by FIELD_1:39
.= ((emb_iso h) ") . (phi . v) by A1, FUNCT_1:13
.= a by D, A3, FUNCT_1:34 ; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of NAT ;
((PolyHom iso) . (emb (p,p))) . i = iso . ((emb (p,p)) . i) by FIELD_1:def 2
.= iso . (Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((p . i) | F))) by FIELD_1:40
.= iso . ((emb p) . (p . i)) by FIELD_1:39 ;
hence ((PolyHom iso) . (emb (p,p))) . x = p . x by A; :: thesis:

end;

hence (PolyHom iso) . (emb (p,p)) = p ; :: thesis:

end;

then K: Ext_eval (p,a) = 0. E by Z, FIELD_4:26;
then reconsider a1 = a as F -algebraic Element of E by FIELD_6:43;
take a1 = a1; :: thesis:
p = MinPoly (a1,F) by K, FIELD_6:52;
hence ( ex E being FieldExtension of F ex a being F -algebraic Element of E st p1 = MinPoly (a,F) iff ( p1 is monic & p1 is irreducible ) ) ; :: thesis:

end;

hence ( ex E being FieldExtension of F ex a being F -algebraic Element of E st p1 = MinPoly (a,F) iff ( p1 is monic & p1 is irreducible ) ) ; :: thesis: