consider A being FieldExtension of F such that
A:
A is algebraic-closed
by main1;
take K = F_Alg A; ( K is F -algebraic & K is algebraic-closed )
thus
K is F -algebraic
; K is algebraic-closed
now for p being non constant Polynomial of K holds p is with_roots let p be non
constant Polynomial of
K;
p is with_roots reconsider A =
A as
K -extending FieldExtension of
F by FIELD_7:42;
K is
Subfield of
A
by FIELD_4:7;
then H0:
K is
Subring of
A
by FIELD_5:12;
then reconsider p1 =
p as
Polynomial of
A by FIELD_4:9;
H1:
p1 is
Element of
(Polynom-Ring A)
by POLYNOM3:def 10;
H2:
p is
Element of
(Polynom-Ring K)
by POLYNOM3:def 10;
B0:
deg p > 0
by RATFUNC1:def 2;
deg p = deg p1
by H1, H2, FIELD_4:20;
then reconsider p1 =
p1 as non
constant Polynomial of
A by B0, RATFUNC1:def 2;
consider a1 being
Element of
A such that B1:
a1 is_a_root_of p1
by A, POLYNOM5:def 8;
B2:
0. A =
eval (
p1,
a1)
by B1, POLYNOM5:def 7
.=
Ext_eval (
p,
a1)
by H1, H2, FIELD_4:26
;
then
a1 is
F -algebraic
by FIELD_6:43, lemA;
then
a1 in { a where a is F -algebraic Element of A : verum }
;
then
a1 in Alg_El A
by FIELD_7:def 13;
then reconsider a =
a1 as
Element of
K by FIELD_7:def 14;
eval (
p,
a) =
Ext_eval (
p,
a1)
by H2, FIELD_6:10
.=
0. K
by B2, H0, C0SP1:def 3
;
hence
p is
with_roots
by POLYNOM5:def 7, POLYNOM5:def 8;
verum end;
hence
K is algebraic-closed
by alg2; verum