let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for L being algebraic-closed F -monomorphic Field
for f being Monomorphism of F,L ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for L being algebraic-closed F -monomorphic Field
for f being Monomorphism of F,L ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )
let a be F -algebraic Element of E; :: thesis: for L being algebraic-closed F -monomorphic Field
for f being Monomorphism of F,L ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )
let L be algebraic-closed F -monomorphic Field; :: thesis: for f being Monomorphism of F,L ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )
let f be Monomorphism of F,L; :: thesis: ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )

per cases ( a in F or not a in F ) ;

suppose a in F ; :: thesis: ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )

then {a} c= the carrier of F by TARSKI:def 1;
then I: doubleLoopStr(# the carrier of (FAdj (F,{a})), the addF of (FAdj (F,{a})), the multF of (FAdj (F,{a})), the OneF of (FAdj (F,{a})), the ZeroF of (FAdj (F,{a})) #) = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) by FIELD_7:3, FIELD_7:def 1;
then reconsider f1 = f as Function of (FAdj (F,{a})),L ;
take f1 ; :: thesis: ( f1 is monomorphism & f1 is f -extending )
( f1 is additive & f1 is multiplicative & f1 is unity-preserving )

proof

now :: thesis: for x, y being Element of (FAdj (F,{a})) holds f1 . (x + y) = (f1 . x) + (f1 . y)

let x, y be Element of (FAdj (F,{a})); :: thesis: f1 . (x + y) = (f1 . x) + (f1 . y)
reconsider x1 = x, y1 = y as Element of F by I;
x + y = x1 + y1 by I;
hence f1 . (x + y) = (f1 . x) + (f1 . y) by VECTSP_1:def 20; :: thesis: verum

end;

hence f1 is additive ; :: thesis: ( f1 is multiplicative & f1 is unity-preserving )

now :: thesis: for x, y being Element of (FAdj (F,{a})) holds f1 . (x * y) = (f1 . x) * (f1 . y)

let x, y be Element of (FAdj (F,{a})); :: thesis: f1 . (x * y) = (f1 . x) * (f1 . y)
reconsider x1 = x, y1 = y as Element of F by I;
x * y = x1 * y1 by I;
hence f1 . (x * y) = (f1 . x) * (f1 . y) by GROUP_6:def 6; :: thesis: verum

end;

hence f1 is multiplicative ; :: thesis: f1 is unity-preserving
1_ (FAdj (F,{a})) = 1_ F by I;
hence f1 is unity-preserving by GROUP_1:def 13; :: thesis: verum

end;

hence ( f1 is monomorphism & f1 is f -extending ) ; :: thesis: verum

end;

suppose not a in F ; :: thesis: ex g being Function of (FAdj (F,{a})),L st
( g is monomorphism & g is f -extending )

reconsider L1 = L as F -homomorphic F -monomorphic FieldExtension of L by FIELD_4:6;
reconsider f1 = f as Monomorphism of F,L1 ;
reconsider p = MinPoly (a,F) as Element of the carrier of (Polynom-Ring F) ;
reconsider q = (PolyHom f1) . p as Polynomial of L ;
deg q >= 0 ;
then reconsider q = q as non constant Polynomial of L by RATFUNC1:def 2, RING_4:def 4;
consider b being Element of L such that
A0: b is_a_root_of q by POLYNOM5:def 8;
eval (q,b) = 0. L by A0, POLYNOM5:def 7;
then B0: Ext_eval (q,b) = 0. L1 by FIELD_6:10;
then reconsider b = b as L -algebraic Element of L1 by FIELD_6:43;
H: FAdj (F,{a}) = RAdj (F,{a}) by FIELD_6:56;
set M = { [(Ext_eval (p,a)),(Ext_eval (q,b))] where p is Polynomial of F, q is Polynomial of L : q = (PolyHom f1) . p } ;

now :: thesis: for o being object st o in { [(Ext_eval (p,a)),(Ext_eval (q,b))] where p is Polynomial of F, q is Polynomial of L : q = (PolyHom f1) . p } holds
o in [: the carrier of (FAdj (F,{a})), the carrier of L:]

let o be object ; :: thesis: ( o in { [(Ext_eval (p,a)),(Ext_eval (q,b))] where p is Polynomial of F, q is Polynomial of L : q = (PolyHom f1) . p } implies o in [: the carrier of (FAdj (F,{a})), the carrier of L:] )
assume o in { [(Ext_eval (p,a)),(Ext_eval (q,b))] where p is Polynomial of F, q is Polynomial of L : q = (PolyHom f1) . p } ; :: thesis: o in [: the carrier of (FAdj (F,{a})), the carrier of L:]
then consider p being Polynomial of F, q being Polynomial of L such that
A: ( o = [(Ext_eval (p,a)),(Ext_eval (q,b))] & q = (PolyHom f1) . p ) ;
Ext_eval (p,a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ;
then B: Ext_eval (p,a) in the carrier of (FAdj (F,{a})) by H, FIELD_6:45;
thus o in [: the carrier of (FAdj (F,{a})), the carrier of L:] by A, B, ZFMISC_1:def 2; :: thesis: verum

end;

then { [(Ext_eval (p,a)),(Ext_eval (q,b))] where p is Polynomial of F, q is Polynomial of L : q = (PolyHom f1) . p } c= [: the carrier of (FAdj (F,{a})), the carrier of L:] ;
then reconsider M = { [(Ext_eval (p,a)),(Ext_eval (q,b))] where p is Polynomial of F, q is Polynomial of L : q = (PolyHom f1) . p } as Relation of the carrier of (FAdj (F,{a})), the carrier of L ;

now :: thesis: for x, y1, y2 being object st [x,y1] in M & [x,y2] in M holds
y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in M & [x,y2] in M implies y1 = y2 )
assume A1: ( [x,y1] in M & [x,y2] in M ) ; :: thesis: y1 = y2
then consider p1 being Polynomial of F, q1 being Polynomial of L such that
A2: ( [x,y1] = [(Ext_eval (p1,a)),(Ext_eval (q1,b))] & q1 = (PolyHom f1) . p1 ) ;
A3: ( x = Ext_eval (p1,a) & y1 = Ext_eval (q1,b) ) by A2, XTUPLE_0:1;
consider p2 being Polynomial of F, q2 being Polynomial of L such that
A4: ( [x,y2] = [(Ext_eval (p2,a)),(Ext_eval (q2,b))] & q2 = (PolyHom f1) . p2 ) by A1;
A5: ( x = Ext_eval (p2,a) & y2 = Ext_eval (q2,b) ) by A4, XTUPLE_0:1;
Ext_eval (p1,a) = Ext_eval (p2,a) by A2, XTUPLE_0:1, A5;
then A6: 0. E = (Ext_eval (p1,a)) - (Ext_eval (p2,a)) by RLVECT_1:15
.= Ext_eval ((p1 - p2),a) by FIELD_6:27 ;
reconsider pm = p1 - p2 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
A7: (PolyHom f1) . p divides (PolyHom f1) . pm by A6, FIELD_6:53, F814;
A8: Ext_eval ((q1 - q2),b) = 0. L

proof

reconsider u = (PolyHom f1) . p as Polynomial of L ;
consider v being Polynomial of L such that
V: u *' v = (PolyHom f1) . pm by A7, RING_4:1;
reconsider p1a = p1, p2a = p2 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
- p2 = - p2a by FIELD_8:1;
then Z: p1 - p2 = p1a - p2a by POLYNOM3:def 10;
Y: - q2 = - ((PolyHom f1) . p2a) by A4, FIELD_8:1;
X: q1 - q2 = ((PolyHom f1) . p1a) + (- ((PolyHom f1) . p2a)) by Y, A2, POLYNOM3:def 10
.= ((PolyHom f1) . p1a) + ((PolyHom f1) . (- p2a)) by F815
.= (PolyHom f1) . pm by Z, FIELD_1:24 ;
L is Subfield of L1 by FIELD_4:7;
then W: L is Subring of L1 by FIELD_5:12;
Ext_eval (((PolyHom f1) . pm),b) = (0. L1) * (Ext_eval (v,b)) by B0, V, W, ALGNUM_1:20;
hence Ext_eval ((q1 - q2),b) = 0. L by X; :: thesis: verum

end;

0. L = (Ext_eval (q1,b)) - (Ext_eval (q2,b)) by A8, FIELD_6:27;
hence y1 = y2 by A5, A3, RLVECT_1:21; :: thesis: verum

end;

then reconsider g = M as Function by FUNCT_1:def 1;
A1: for o being object st o in dom M holds
o in the carrier of (FAdj (F,{a})) ;

now :: thesis: for o being object st o in the carrier of (FAdj (F,{a})) holds
o in dom g

let o be object ; :: thesis: ( o in the carrier of (FAdj (F,{a})) implies o in dom g )
assume o in the carrier of (FAdj (F,{a})) ; :: thesis: o in dom g
then o in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider p being Polynomial of F such that
A: o = Ext_eval (p,a) ;
ex y being object st [o,y] in g

proof

reconsider p1 = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider q = (PolyHom f1) . p1 as Polynomial of L ;
take y = Ext_eval (q,b); :: thesis: [o,y] in g
thus [o,y] in g by A; :: thesis: verum

end;

hence o in dom g by XTUPLE_0:def 12; :: thesis: verum

end;

then A2: dom g = the carrier of (FAdj (F,{a})) by A1, TARSKI:2;
rng M is Subset of the carrier of L ;
then reconsider g = g as Function of the carrier of (FAdj (F,{a})), the carrier of L by A2, FUNCT_2:2;
U: for p being Polynomial of F
for q being Polynomial of L st q = (PolyHom f1) . p holds
g . (Ext_eval (p,a)) = Ext_eval (q,b)

proof

let p be Polynomial of F; :: thesis: for q being Polynomial of L st q = (PolyHom f1) . p holds
g . (Ext_eval (p,a)) = Ext_eval (q,b)
let q be Polynomial of L; :: thesis: ( q = (PolyHom f1) . p implies g . (Ext_eval (p,a)) = Ext_eval (q,b) )
assume q = (PolyHom f1) . p ; :: thesis: g . (Ext_eval (p,a)) = Ext_eval (q,b)
then [(Ext_eval (p,a)),(Ext_eval (q,b))] in g ;
hence g . (Ext_eval (p,a)) = Ext_eval (q,b) by FUNCT_1:1; :: thesis: verum

end;

take g ; :: thesis: ( g is monomorphism & g is f -extending )
I4: L is Subring of L1 by FIELD_4:def 1;

C1: now :: thesis: for x, y being Element of (FAdj (F,{a})) holds g . (x + y) = (g . x) + (g . y)

let x, y be Element of (FAdj (F,{a})); :: thesis: g . (x + y) = (g . x) + (g . y)
x in the carrier of (FAdj (F,{a})) ;
then x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider p being Polynomial of F such that
A1: x = Ext_eval (p,a) ;
y in the carrier of (FAdj (F,{a})) ;
then y in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider q being Polynomial of F such that
A2: y = Ext_eval (q,a) ;
reconsider pF = p, qF = q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider f1p = (PolyHom f1) . pF, f1q = (PolyHom f1) . qF as Polynomial of L ;
B: ( g . x = Ext_eval (f1p,b) & g . y = Ext_eval (f1q,b) ) by A1, A2, U;
D: x + y = Ext_eval ((p + q),a) by A1, A2, FIELD_8:47;
reconsider pqF = p + q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider f1pq = (PolyHom f1) . (pF + qF) as Polynomial of L ;
E: (PolyHom f1) . (pF + qF) = ((PolyHom f1) . pF) + ((PolyHom f1) . qF) by FIELD_1:24
.= f1p + f1q by POLYNOM3:def 10 ;
F: p + q = pF + qF by POLYNOM3:def 10;
thus g . (x + y) = Ext_eval ((f1p + f1q),b) by D, U, E, F
.= (g . x) + (g . y) by B, I4, ALGNUM_1:15 ; :: thesis: verum

end;

C2: now :: thesis: for x, y being Element of (FAdj (F,{a})) holds g . (x * y) = (g . x) * (g . y)

let x, y be Element of (FAdj (F,{a})); :: thesis: g . (x * y) = (g . x) * (g . y)
x in the carrier of (FAdj (F,{a})) ;
then x in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider p being Polynomial of F such that
A1: x = Ext_eval (p,a) ;
y in the carrier of (FAdj (F,{a})) ;
then y in { (Ext_eval (p,a)) where p is Polynomial of F : verum } by H, FIELD_6:45;
then consider q being Polynomial of F such that
A2: y = Ext_eval (q,a) ;
reconsider pF = p, qF = q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider f1p = (PolyHom f1) . pF, f1q = (PolyHom f1) . qF as Polynomial of L ;
B: ( g . x = Ext_eval (f1p,b) & g . y = Ext_eval (f1q,b) ) by A1, A2, U;
D: x * y = Ext_eval ((p *' q),a) by A1, A2, FIELD_8:47;
reconsider pqF = p *' q as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider f1pq = (PolyHom f1) . (pF * qF) as Polynomial of L ;
E: (PolyHom f1) . (pF * qF) = ((PolyHom f1) . pF) * ((PolyHom f1) . qF) by FIELD_1:25
.= f1p *' f1q by POLYNOM3:def 10 ;
F: p *' q = pF * qF by POLYNOM3:def 10;
thus g . (x * y) = Ext_eval ((f1p *' f1q),b) by D, U, E, F
.= (g . x) * (g . y) by B, I4, ALGNUM_1:20 ; :: thesis: verum

end;

C3: g . (1_ (FAdj (F,{a}))) = 1_ L1

proof

reconsider g1 = (1. F) | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider q = (1. L) | L as Element of the carrier of (Polynom-Ring L) by POLYNOM3:def 10;
F: f . (1_ F) = 1_ L by GROUP_1:def 13;
1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) by FIELD_8:46
.= Ext_eval (g1,a) by RING_4:14 ;
then g . (1. (FAdj (F,{a}))) = Ext_eval (((PolyHom f1) . g1),b) by U
.= Ext_eval (q,b) by F, FIELD_8:13
.= LC ((1. L) | L) by FIELD_6:28
.= 1. L1 by FIELD_8:3 ;
hence g . (1_ (FAdj (F,{a}))) = 1_ L1 ; :: thesis: verum

end;

C: ( g is additive & g is multiplicative & g is unity-preserving ) by C1, C2, C3;

now :: thesis: for x being Element of F holds g . x = f . x

let x be Element of F; :: thesis: g . x = f . x
reconsider g1 = x | F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
x = Ext_eval ((x | F),a) by FIELD_8:48;
hence g . x = Ext_eval (((PolyHom f1) . g1),b) by U
.= Ext_eval (((f . x) | L),b) by FIELD_8:13
.= LC ((f . x) | L) by FIELD_6:28
.= f . x by FIELD_8:3 ;
:: thesis: verum

end;

hence ( g is monomorphism & g is f -extending ) by C; :: thesis: verum

end;

end;