now for p being non constant Polynomial of (SeqField f) holds p is with_roots let p be non
constant Polynomial of
(SeqField f);
p is with_roots consider i being
Element of
NAT such that A:
p is non
constant Polynomial of
(f . i)
by f12;
reconsider F =
f . i as
Field ;
reconsider q =
p as non
constant Polynomial of
F by A;
reconsider p1 =
q as
Element of the
carrier of
(Polynom-Ring F) by POLYNOM3:def 10;
deg q >= 0
;
then reconsider p1 =
p1 as non
constant Element of the
carrier of
(Polynom-Ring F) by RING_4:def 4, RATFUNC1:def 2;
reconsider E =
f . (i + 1) as
FieldExtension of
F by defasc;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider q1 =
p1 as
Element of the
carrier of
(Polynom-Ring E) ;
consider a being
Element of
E such that B:
a is_a_root_of p1,
E
by dA, FIELD_4:def 3;
C:
Ext_eval (
p1,
a)
= 0. E
by B, FIELD_4:def 2;
D:
F is
Subfield of
SeqField f
by Fsub;
reconsider pp =
p as
Element of the
carrier of
(Polynom-Ring (SeqField f)) by POLYNOM3:def 10;
G:
E is
Subfield of
SeqField f
by Fsub;
then
the
carrier of
E c= the
carrier of
(SeqField f)
by EC_PF_1:def 1;
then reconsider a1 =
a as
Element of
(SeqField f) ;
F:
SeqField f is
E -extending FieldExtension of
F
by G, D, FIELD_4:7;
then Ext_eval (
p1,
a) =
Ext_eval (
p1,
a1)
by FIELD_7:14
.=
eval (
pp,
a1)
by F, FIELD_4:26
.=
eval (
p,
a1)
;
then
eval (
p,
a1)
= 0. (SeqField f)
by C, G, EC_PF_1:def 1;
hence
p is
with_roots
by POLYNOM5:def 8, POLYNOM5:def 7;
verum end;
hence
SeqField f is algebraic-closed
by alg2; verum