let F be Field; :: thesis: for A being AlgebraicClosure of F
for L being b₁ -homomorphic b₁ -monomorphic Field
for g being Monomorphism of A,L holds Image g is algebraic-closed
let E be AlgebraicClosure of F; :: thesis: for L being E -homomorphic E -monomorphic Field
for g being Monomorphism of E,L holds Image g is algebraic-closed
let L be E -homomorphic E -monomorphic Field; :: thesis: for g being Monomorphism of E,L holds Image g is algebraic-closed
let g be Monomorphism of E,L; :: thesis: Image g is algebraic-closed
H: rng g = the carrier of (Image g) by RING_2:def 6;
then reconsider f = g " as Function of (Image g),E ;
A: ( f is additive & f is multiplicative & f is unity-preserving & f is monomorphism )

proof

B1: now :: thesis: for a, b being Element of (Image g) holds f . (a + b) = (f . a) + (f . b)

let a, b be Element of (Image g); :: thesis: f . (a + b) = (f . a) + (f . b)
consider x being object such that
A1: ( x in dom g & g . x = a ) by H, FUNCT_1:def 3;
reconsider x = x as Element of E by A1;
consider y being object such that
A2: ( y in dom g & g . y = b ) by H, FUNCT_1:def 3;
reconsider y = y as Element of E by A2;
A3: dom g = the carrier of E by FUNCT_2:def 1;
A4: (g ") . b = y by A2, FUNCT_1:34;
A5: [a,b] in [: the carrier of (Image g), the carrier of (Image g):] by ZFMISC_1:def 2;
g . (x + y) = (g . x) + (g . y) by VECTSP_1:def 20
.= ( the addF of L || the carrier of (Image g)) . (a,b) by A1, A2, A5, FUNCT_1:49
.= a + b by EC_PF_1:def 1 ;
hence f . (a + b) = x + y by A3, FUNCT_1:34
.= (f . a) + (f . b) by A1, A4, FUNCT_1:34 ;
:: thesis: verum

end;

B2: now :: thesis: for a, b being Element of (Image g) holds f . (a * b) = (f . a) * (f . b)

let a, b be Element of (Image g); :: thesis: f . (a * b) = (f . a) * (f . b)
consider x being object such that
A1: ( x in dom g & g . x = a ) by H, FUNCT_1:def 3;
reconsider x = x as Element of E by A1;
consider y being object such that
A2: ( y in dom g & g . y = b ) by H, FUNCT_1:def 3;
reconsider y = y as Element of E by A2;
A3: dom g = the carrier of E by FUNCT_2:def 1;
A4: (g ") . b = y by A2, FUNCT_1:34;
A5: [a,b] in [: the carrier of (Image g), the carrier of (Image g):] by ZFMISC_1:def 2;
g . (x * y) = (g . x) * (g . y) by GROUP_6:def 6
.= ( the multF of L || the carrier of (Image g)) . (a,b) by A1, A2, A5, FUNCT_1:49
.= a * b by EC_PF_1:def 1 ;
hence f . (a * b) = x * y by A3, FUNCT_1:34
.= (f . a) * (f . b) by A1, A4, FUNCT_1:34 ;
:: thesis: verum

end;

B3: dom g = the carrier of E by FUNCT_2:def 1;
g . (1_ E) = 1_ L by GROUP_1:def 13
.= 1_ (Image g) by EC_PF_1:def 1 ;
then ( f is additive & f is multiplicative & f is unity-preserving ) by B1, B2, B3, FUNCT_1:34;
hence ( f is additive & f is multiplicative & f is unity-preserving & f is monomorphism ) ; :: thesis: verum

end;

then reconsider E1 = E as Image g -homomorphic Image g -monomorphic Field by RING_2:def 4, RING_3:def 3;
reconsider f = f as Monomorphism of (Image g),E1 by A;

now :: thesis: for p being non constant Polynomial of (Image g) holds p is with_roots

let p be non constant Polynomial of (Image g); :: thesis: p is with_roots
reconsider p1 = p as Element of the carrier of (Polynom-Ring (Image g)) by POLYNOM3:def 10;
C: deg p > 0 by RATFUNC1:def 2;
then reconsider p1 = p1 as non constant Element of the carrier of (Polynom-Ring (Image g)) by RING_4:def 4;
reconsider q = (PolyHom f) . p1 as Polynomial of E ;
deg p1 = deg ((PolyHom f) . p1) by FIELD_1:31;
then reconsider q = (PolyHom f) . p1 as non constant Polynomial of E by C, RATFUNC1:def 2;
consider a being Element of E such that
B: a is_a_root_of q by POLYNOM5:def 8;
reconsider r = q as Element of the carrier of (Polynom-Ring E) ;
F: dom (PolyHom f) = the carrier of (Polynom-Ring (Image g)) by FUNCT_2:def 1;
E: (PolyHom g) . ((PolyHom f) . p1) = p1

proof

dom g = the carrier of E1 by FUNCT_2:def 1;
then reconsider g1 = g as Function of E1,(Image g) by H, FUNCT_2:1;
Z: ( g1 is additive & g1 is multiplicative & g1 is unity-preserving )

proof

now :: thesis: for a, b being Element of E1 holds g1 . (a + b) = (g1 . a) + (g1 . b)

let a, b be Element of E1; :: thesis: g1 . (a + b) = (g1 . a) + (g1 . b)
reconsider a1 = a, b1 = b as Element of E ;
Z1: [(g1 . a),(g1 . b)] in [: the carrier of (Image g), the carrier of (Image g):] by ZFMISC_1:def 2;
thus g1 . (a + b) = (g . a1) + (g . b1) by VECTSP_1:def 20
.= ( the addF of L || the carrier of (Image g)) . ((g1 . a),(g1 . b)) by Z1, FUNCT_1:49
.= (g1 . a) + (g1 . b) by EC_PF_1:def 1 ; :: thesis: verum

end;

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

now :: thesis: for a, b being Element of E1 holds g1 . (a * b) = (g1 . a) * (g1 . b)

let a, b be Element of E1; :: thesis: g1 . (a * b) = (g1 . a) * (g1 . b)
reconsider a1 = a, b1 = b as Element of E ;
Z1: [(g1 . a),(g1 . b)] in [: the carrier of (Image g), the carrier of (Image g):] by ZFMISC_1:def 2;
thus g1 . (a * b) = (g . a1) * (g . b1) by GROUP_6:def 6
.= ( the multF of L || the carrier of (Image g)) . ((g1 . a),(g1 . b)) by Z1, FUNCT_1:49
.= (g1 . a) * (g1 . b) by EC_PF_1:def 1 ; :: thesis: verum

end;

hence g1 is multiplicative ; :: thesis: g1 is unity-preserving
g1 . (1_ E1) = 1_ L by GROUP_1:def 13
.= 1_ (Image g) by EC_PF_1:def 1 ;
hence g1 is unity-preserving ; :: thesis: verum

end;

reconsider Ig = Image g as E1 -homomorphic Field by Z, RING_2:def 4;
reconsider g1 = g1 as additive Function of E1,Ig by Z;
G: g1 * f = id (Image g)

proof

now :: thesis: for o being object st o in dom (g1 * f) holds
(g1 * f) . o = (id (Image g)) . o

let o be object ; :: thesis: ( o in dom (g1 * f) implies (g1 * f) . o = (id (Image g)) . o )
assume o in dom (g1 * f) ; :: thesis: (g1 * f) . o = (id (Image g)) . o
then reconsider a = o as Element of (Image g) ;
(g1 * f) . a = a by H, FUNCT_1:35;
hence (g1 * f) . o = (id (Image g)) . o ; :: thesis: verum

end;

hence g1 * f = id (Image g) by FUNCT_2:def 1; :: thesis: verum

end;

H: PolyHom g1 = PolyHom g

proof

now :: thesis: for o being object st o in the carrier of (Polynom-Ring E1) holds
(PolyHom g1) . o = (PolyHom g) . o

let o be object ; :: thesis: ( o in the carrier of (Polynom-Ring E1) implies (PolyHom g1) . o = (PolyHom g) . o )
assume o in the carrier of (Polynom-Ring E1) ; :: thesis: (PolyHom g1) . o = (PolyHom g) . o
then reconsider a = o as Element of the carrier of (Polynom-Ring E1) ;
reconsider b = a as Element of the carrier of (Polynom-Ring E) ;

now :: thesis: for i being Nat holds ((PolyHom g) . b) . i = ((PolyHom g1) . a) . i

let i be Nat; :: thesis: ((PolyHom g) . b) . i = ((PolyHom g1) . a) . i
thus ((PolyHom g) . b) . i = g . (b . i) by FIELD_1:def 2
.= ((PolyHom g1) . a) . i by FIELD_1:def 2 ; :: thesis: verum

end;

then (PolyHom g1) . a = (PolyHom g) . b ;
hence (PolyHom g1) . o = (PolyHom g) . o ; :: thesis: verum

end;

hence PolyHom g1 = PolyHom g ; :: thesis: verum

end;

thus (PolyHom g) . ((PolyHom f) . p1) = ((PolyHom g1) * (PolyHom f)) . p1 by F, H, FUNCT_1:13
.= (id (Polynom-Ring (Image g))) . p1 by G, ll2
.= p1 ; :: thesis: verum

end;

dom g = the carrier of E by FUNCT_2:def 1;
then reconsider ga = g . a as Element of (Image g) by H, FUNCT_1:3;
L is FieldExtension of Image g by FIELD_4:7;
then eval (p,ga) = eval (((PolyHom g) . r),(g . a)) by E, FIELD_4:27
.= 0. L by B, FIELD_1:34, POLYNOM5:def 7
.= 0. (Image g) by RING_2:def 6 ;
hence p is with_roots by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum

end;

hence Image g is algebraic-closed by alg2; :: thesis: verum