let E be FieldExtension of F; :: thesis:
assume deg (E,F) = (2 * 0) + 1 ; :: thesis:
then E == F by FIELD_7:8;
then ex Q being Subset of E st
( Q = P & Q is positive_cone ) by lemPP;
hence P extends_to E ; :: thesis:

end;

hence S₁[k] by AS2; :: thesis:

end;

suppose AS2: k > 0 ; :: thesis:

let E1 be FieldExtension of F; :: thesis:
assume AS3: deg (E1,F) = (2 * k) + 1 ; :: thesis:
then VecSp (E1,F) is finite-dimensional by FIELD_4:def 7;
then reconsider E = E1 as F -finite FieldExtension of F by FIELD_4:def 8;
consider a being Element of E such that
A0: E == FAdj (F,{a}) by FIELD_14:def 7;
A1: deg (MinPoly (a,F)) = deg ((FAdj (F,{a})),F) by FIELD_6:67
.= deg (E,F) by A0, FIELD_7:5 ;

assume - (1. E) in QS (E,P) ; :: thesis:
then consider f being non empty P -quadratic FinSequence of E such that
A: ( - (1. E) = Sum f & ( for i being Element of NAT st i in dom f holds
f . i <> 0. E ) ) by lemmaA;
ex fc, fd being non empty FinSequence of E st
( len fc = len f & len fd = len f & ( for i being Element of dom fc ex j being Element of dom fd st
( j = i & fc . i in P & fc . i <> 0. E & f . i = (fc . i) * ((fd . j) * (fd . j)) ) ) )

defpred S₂[ Nat] means for f being non empty P -quadratic FinSequence of E st len f = $1 holds
ex fc, fd being non empty FinSequence of E st
( len fc = len f & len fd = len f & ( for i being Element of dom fc ex j being Element of dom fd st
( j = i & fc . i in P & fc . i <> 0. E & f . i = (fc . i) * ((fd . j) * (fd . j)) ) ) );
IA: S₂[1]

let f be non empty P -quadratic FinSequence of E; :: thesis:
assume B0: len f = 1 ; :: thesis:
then f = <*(f . 1)*> by FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:38;
then consider a being non zero Element of E, b being Element of E such that
B1: ( a in P & f . 1 = a * (b ^2) ) by FINSEQ_1:3, dq;
reconsider fc = <*a*>, fd = <*b*> as non empty FinSequence of E ;
B2: ( len fc = 1 & len fd = 1 ) by FINSEQ_1:40;

B3: now :: thesis:

let i be Element of dom fc; :: thesis:
B5: dom fc = Seg 1 by FINSEQ_1:38;
then B4: i = 1 by FINSEQ_1:2, TARSKI:def 1;
dom fd = Seg 1 by FINSEQ_1:38;
then reconsider j = 1 as Element of dom fd by FINSEQ_1:2, TARSKI:def 1;
thus ex j being Element of dom fd st
( j = i & fc . i in P & fc . i <> 0. E & f . i = (fc . i) * ((fd . j) * (fd . j)) ) :: thesis:

take j ; :: thesis:
thus j = i by B5, FINSEQ_1:2, TARSKI:def 1; :: thesis:
thus fc . i in P by B4, B1; :: thesis:
thus fc . i <> 0. E by B4; :: thesis:
thus (fc . i) * ((fd . j) * (fd . j)) = a * ((fd . j) * (fd . j)) by B4
.= a * (b * (fd . j))
.= f . i by B4, B1 ; :: thesis:

end;

thus ex fc, fd being non empty FinSequence of E st
( len fc = len f & len fd = len f & ( for i being Element of dom fc ex j being Element of dom fd st
( j = i & fc . i in P & fc . i <> 0. E & f . i = (fc . i) * ((fd . j) * (fd . j)) ) ) ) by B0, B2, B3; :: thesis:

end;

hence S₂[1] ; :: thesis:

end;

IS: now :: thesis:

let k be Nat; :: thesis:
assume IV1: k >= 1 ; :: thesis:
assume IV: S₂[k] ; :: thesis:

let f be non empty P -quadratic FinSequence of E; :: thesis:
assume AS: len f = k + 1 ; :: thesis:
consider G being FinSequence, y being object such that
B2: f = G ^ <*y*> by FINSEQ_1:46;
rng G c= rng f by B2, FINSEQ_1:29;
then reconsider G = G as FinSequence of E by XBOOLE_1:1, FINSEQ_1:def 4;
B10: len f = (len G) + (len <*y*>) by B2, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
reconsider G = G as non empty FinSequence of E by B10, AS, IV1;
reconsider r = <*y*> as non empty FinSequence of E by B2, FINSEQ_1:36;
f = G ^ r by B2;
then reconsider G = G, r = r as non empty P -quadratic FinSequence of E by XYZbS3a;
consider Gfc, Gfd being non empty FinSequence of E such that
II: ( len Gfc = len G & len Gfd = len G & ( for i being Element of dom Gfc ex j being Element of dom Gfd st
( j = i & Gfc . i in P & Gfc . i <> 0. E & G . i = (Gfc . i) * ((Gfd . j) * (Gfd . j)) ) ) ) by AS, B10, IV;
rng <*y*> = {y} by FINSEQ_1:39;
then G5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng f by B2, FINSEQ_1:30;
then consider u being object such that
G6: ( u in dom f & f . u = y ) by G5, FUNCT_1:def 3;
reconsider u = u as Element of NAT by G6;
( f . u in rng f & rng f c= the carrier of E ) by G6, FUNCT_1:3;
then reconsider y = y as Element of E by G6;
consider yc being non zero Element of E, yd being Element of E such that
G7: ( yc in P & f . u = yc * (yd ^2) ) by G6, dq;
set fc = Gfc ^ <*yc*>;
set fd = Gfd ^ <*yd*>;
D1: len (Gfc ^ <*yc*>) = (len Gfc) + (len <*yc*>) by FINSEQ_1:22
.= len f by II, B10, FINSEQ_1:39 ;
D2: len (Gfd ^ <*yd*>) = (len Gfd) + (len <*yd*>) by FINSEQ_1:22
.= len f by II, B10, FINSEQ_1:39 ;

D3: now :: thesis:

let i be Element of dom (Gfc ^ <*yc*>); :: thesis:
dom (Gfc ^ <*yc*>) = Seg (len (Gfd ^ <*yd*>)) by D2, D1, FINSEQ_1:def 3;
then reconsider jj = i as Element of dom (Gfd ^ <*yd*>) by FINSEQ_1:def 3;

per cases ;

suppose E: i in dom Gfc ; :: thesis:

then reconsider i1 = i as Element of dom Gfc ;
consider j being Element of dom Gfd such that
F: ( j = i1 & Gfc . i1 in P & Gfc . i1 <> 0. E & G . i1 = (Gfc . i1) * ((Gfd . j) * (Gfd . j)) ) by II;
thus ex j being Element of dom (Gfd ^ <*yd*>) st
( j = i & (Gfc ^ <*yc*>) . i in P & (Gfc ^ <*yc*>) . i <> 0. E & f . i = ((Gfc ^ <*yc*>) . i) * (((Gfd ^ <*yd*>) . j) * ((Gfd ^ <*yd*>) . j)) ) :: thesis:

take jj ; :: thesis:
thus jj = i ; :: thesis:
G: (Gfc ^ <*yc*>) . i = Gfc . i by E, FINSEQ_1:def 7;
H: (Gfd ^ <*yd*>) . jj = Gfd . j by F, FINSEQ_1:def 7;
thus (Gfc ^ <*yc*>) . i in P by F, FINSEQ_1:def 7; :: thesis:
thus (Gfc ^ <*yc*>) . i <> 0. E by F, FINSEQ_1:def 7; :: thesis:
dom G = Seg (len Gfc) by II, FINSEQ_1:def 3;
then i in dom G by E, FINSEQ_1:def 3;
hence f . i = ((Gfc ^ <*yc*>) . i) * (((Gfd ^ <*yd*>) . jj) * ((Gfd ^ <*yd*>) . jj)) by G, H, F, B2, FINSEQ_1:def 7; :: thesis:

end;

suppose E: not i in dom Gfc ; :: thesis:

E1: dom Gfc = Seg (len G) by II, FINSEQ_1:def 3;
dom (Gfc ^ <*yc*>) = Seg (len f) by D1, FINSEQ_1:def 3;
then E5: ( 1 <= i & i <= len f ) by FINSEQ_1:1;

E2: now :: thesis:

assume i <> (len G) + 1 ; :: thesis:
then i < (len G) + 1 by E5, B10, XXREAL_0:1;
then (i + 1) - 1 <= ((len G) + 1) - 1 by INT_1:7;
hence contradiction by E1, E5, E, FINSEQ_1:1; :: thesis:

end;

dom <*y*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*y*> by FINSEQ_1:3;
then E3: f . i = <*y*> . 1 by B2, E2, FINSEQ_1:def 7
.= yc * (yd ^2) by G7, G6 ;
dom <*yc*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*yc*> by FINSEQ_1:3;
then E6: (Gfc ^ <*yc*>) . i = <*yc*> . 1 by II, E2, FINSEQ_1:def 7
.= yc ;
dom <*yd*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*yd*> by FINSEQ_1:3;
then E7: (Gfd ^ <*yd*>) . i = <*yd*> . 1 by II, E2, FINSEQ_1:def 7
.= yd ;
thus ex j being Element of dom (Gfd ^ <*yd*>) st
( j = i & (Gfc ^ <*yc*>) . i in P & (Gfc ^ <*yc*>) . i <> 0. E & f . i = ((Gfc ^ <*yc*>) . i) * (((Gfd ^ <*yd*>) . j) * ((Gfd ^ <*yd*>) . j)) ) :: thesis:

take jj ; :: thesis:
thus jj = i ; :: thesis:
thus (Gfc ^ <*yc*>) . i in P by E6, G7; :: thesis:
thus (Gfc ^ <*yc*>) . i <> 0. E by E6; :: thesis:
thus f . i = ((Gfc ^ <*yc*>) . i) * (((Gfd ^ <*yd*>) . jj) * ((Gfd ^ <*yd*>) . jj)) by E3, E6, E7; :: thesis:

end;

hence S₂[k + 1] ; :: thesis:

end;

I: for k being Nat st k >= 1 holds
S₂[k] from NAT_1:sch 8(IA, IS);
len f >= 0 + 1 by INT_1:7;
hence ex fc, fd being non empty FinSequence of E st
( len fc = len f & len fd = len f & ( for i being Element of dom fc ex j being Element of dom fd st
( j = i & fc . i in P & fc . i <> 0. E & f . i = (fc . i) * ((fd . j) * (fd . j)) ) ) ) by I; :: thesis:

end;

then consider fc, fd being non empty FinSequence of E such that
U: ( len fc = len f & len fd = len f & ( for i being Element of dom fc ex j being Element of dom fd st
( j = i & fc . i in P & fc . i <> 0. E & f . i = (fc . i) * ((fd . j) * (fd . j)) ) ) ) ;
ex g1 being non empty FinSequence of the carrier of (Polynom-Ring F) st
( len g1 = len f & ( for i being Element of dom g1 holds
( not g1 . i is zero & deg (g1 . i) < deg (MinPoly (a,F)) & fd . i = Ext_eval ((g1 . i),a) ) ) )

defpred S₂[ Nat, object ] means ex q being Polynomial of F st
( q = $2 & not q is zero & deg q < deg (MinPoly (a,F)) & fd . $1 = Ext_eval (q,a) );

let k be Nat; :: thesis:
assume k in Seg (len f) ; :: thesis:
then reconsider jd = k as Element of dom fd by U, FINSEQ_1:def 3;
thus ex x being Element of the carrier of (Polynom-Ring F) st S₂[k,x] :: thesis:

fd . jd in the carrier of (FAdj (F,{a})) by A0;
then reconsider b = fd . k as Element of E ;
consider q being Polynomial of F such that
N1: ( deg q < deg (MinPoly (a,F)) & b = Ext_eval (q,a) ) by A0, lemma;

N2: now :: thesis:

assume q is zero ; :: thesis:
then q = 0_. F by UPROOTS:def 5;
then N3: b = 0. E by N1, ALGNUM_1:13;
dom fc = Seg (len fd) by U, FINSEQ_1:def 3;
then reconsider jc = jd as Element of dom fc by FINSEQ_1:def 3;
dom fc = Seg (len f) by U, FINSEQ_1:def 3;
then reconsider i = jc as Element of dom f by FINSEQ_1:def 3;
consider j being Element of dom fd such that
N4: ( j = jc & fc . jc in P & fc . jc <> 0. E & f . jc = (fc . jc) * ((fd . j) * (fd . j)) ) by U;
f . i = 0. E by N3, N4;
hence contradiction by A; :: thesis:

end;

take q ; :: thesis:
thus ( q is Element of the carrier of (Polynom-Ring F) & S₂[k,q] ) by N1, N2, POLYNOM3:def 10; :: thesis:

end;

consider p being FinSequence of the carrier of (Polynom-Ring F) such that
M: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S₂[k,p . k] ) ) from FINSEQ_1:sch 5(N);
reconsider p = p as non empty FinSequence of the carrier of (Polynom-Ring F) by M;
take p ; :: thesis:

let i be Element of dom p; :: thesis:
reconsider k = i as Nat ;
S₂[k,p . k] by M;
hence ( not p . i is zero & deg (p . i) < deg (MinPoly (a,F)) & fd . i = Ext_eval ((p . i),a) ) ; :: thesis:

end;

hence ( len p = len f & ( for i being Element of dom p holds
( not p . i is zero & deg (p . i) < deg (MinPoly (a,F)) & fd . i = Ext_eval ((p . i),a) ) ) ) by M, FINSEQ_1:def 3; :: thesis:

end;

then consider g1 being non empty FinSequence of the carrier of (Polynom-Ring F) such that
B: ( len g1 = len f & ( for i being Element of dom g1 holds
( not g1 . i is zero & deg (g1 . i) < deg (MinPoly (a,F)) & fd . i = Ext_eval ((g1 . i),a) ) ) ) ;
ex g2 being non empty FinSequence of the carrier of (Polynom-Ring F) st
( len g2 = len g1 & ( for i being Element of dom g1 ex j being Element of dom fc st
( j = i & g2 . i = (@ (F,(fc . j))) * ((g1 . i) *' (g1 . i)) ) ) )

defpred S₂[ Nat, object ] means ex j being Element of dom g1 st
( j = $1 & ex jc being Element of dom fc st
( jc = j & $2 = (@ (F,(fc . jc))) * ((g1 . j) *' (g1 . j)) ) );

let k be Nat; :: thesis:
assume N1: k in Seg (len g1) ; :: thesis:
then reconsider j = k as Element of dom g1 by FINSEQ_1:def 3;
reconsider jc = j as Element of dom fc by B, U, N1, FINSEQ_1:def 3;
thus ex x being Element of the carrier of (Polynom-Ring F) st S₂[k,x] :: thesis:

take x = (@ (F,(fc . jc))) * ((g1 . j) *' (g1 . j)); :: thesis:
thus ( x is Element of the carrier of (Polynom-Ring F) & S₂[k,x] ) by POLYNOM3:def 10; :: thesis:

end;

consider p being FinSequence of the carrier of (Polynom-Ring F) such that
M: ( dom p = Seg (len g1) & ( for k being Nat st k in Seg (len g1) holds
S₂[k,p . k] ) ) from FINSEQ_1:sch 5(N);
reconsider p = p as non empty FinSequence of the carrier of (Polynom-Ring F) by M;
take p ; :: thesis:

let i be Element of dom g1; :: thesis:
reconsider k = i as Nat ;
k in dom g1 ;
then k in Seg (len g1) by FINSEQ_1:def 3;
then S₂[k,p . k] by M;
hence ex j being Element of dom fc st
( j = i & p . i = (@ (F,(fc . j))) * ((g1 . i) *' (g1 . i)) ) ; :: thesis:

end;

hence ( len p = len g1 & ( for i being Element of dom g1 ex j being Element of dom fc st
( j = i & p . i = (@ (F,(fc . j))) * ((g1 . i) *' (g1 . i)) ) ) ) by M, FINSEQ_1:def 3; :: thesis:

end;

then consider g2 being non empty FinSequence of the carrier of (Polynom-Ring F) such that
C: ( len g2 = len g1 & ( for i being Element of dom g1 ex j being Element of dom fc st
( j = i & g2 . i = (@ (F,(fc . j))) * ((g1 . i) *' (g1 . i)) ) ) ) ;
ex g3 being non empty FinSequence of the carrier of E st
( len g3 = len g2 & ( for i being Element of dom g2 holds g3 . i = Ext_eval ((g2 . i),a) ) )

defpred S₂[ Nat, object ] means ex j being Element of dom g2 st
( j = $1 & $2 = Ext_eval ((g2 . j),a) );

let k be Nat; :: thesis:
assume k in Seg (len g2) ; :: thesis:
then reconsider j = k as Element of dom g2 by FINSEQ_1:def 3;
thus ex x being Element of E st S₂[k,x] :: thesis:

take Ext_eval ((g2 . j),a) ; :: thesis:
thus S₂[k, Ext_eval ((g2 . j),a)] ; :: thesis:

end;

consider p being FinSequence of E such that
M: ( dom p = Seg (len g2) & ( for k being Nat st k in Seg (len g2) holds
S₂[k,p . k] ) ) from FINSEQ_1:sch 5(N);
reconsider p = p as non empty FinSequence of E by M;
take p ; :: thesis:

let i be Element of dom g2; :: thesis:
reconsider k = i as Nat ;
k in dom g2 ;
then k in Seg (len g2) by FINSEQ_1:def 3;
then S₂[k,p . k] by M;
hence p . i = Ext_eval ((g2 . i),a) ; :: thesis:

end;

hence ( len p = len g2 & ( for i being Element of dom g2 holds p . i = Ext_eval ((g2 . i),a) ) ) by M, FINSEQ_1:def 3; :: thesis:

end;

then consider g3 being non empty FinSequence of the carrier of E such that
D: ( len g3 = len g2 & ( for i being Element of dom g2 holds g3 . i = Ext_eval ((g2 . i),a) ) ) ;
I0: ( dom f = dom g1 & dom g1 = dom g2 & dom g2 = dom g3 & dom f = dom fc & dom f = dom fd )

dom f = Seg (len g1) by B, FINSEQ_1:def 3;
hence dom f = dom g1 by FINSEQ_1:def 3; :: thesis:
dom g2 = Seg (len g1) by C, FINSEQ_1:def 3;
hence dom g2 = dom g1 by FINSEQ_1:def 3; :: thesis:
dom g2 = Seg (len g3) by D, FINSEQ_1:def 3;
hence dom g2 = dom g3 by FINSEQ_1:def 3; :: thesis:
dom fc = Seg (len f) by U, FINSEQ_1:def 3;
hence dom fc = dom f by FINSEQ_1:def 3; :: thesis:
dom fd = Seg (len f) by U, FINSEQ_1:def 3;
hence dom fd = dom f by FINSEQ_1:def 3; :: thesis:

end;

reconsider q = Sum g2 as Polynomial of F by POLYNOM3:def 10;
set p = (1_. F) + q;
H0: F is Subring of E by FIELD_4:def 1;
H1: (1_. F) + q is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
H2: g3 = f

let j3 be Nat; :: thesis:
assume j3 in dom g3 ; :: thesis:
then reconsider j1 = j3 as Element of dom g1 by I0;
reconsider jc = j1 as Element of dom fc by I0;
consider jd being Element of dom fd such that
H3: ( jd = jc & fc . jc in P & fc . jc <> 0. E & f . jc = (fc . jc) * ((fd . jd) * (fd . jd)) ) by U;
consider j2 being Element of dom fc such that
H5: ( j2 = j1 & g2 . j1 = (@ (F,(fc . j2))) * ((g1 . j1) *' (g1 . j1)) ) by C;
H6: fc . jc is F -membered by H3;
thus g3 . j3 = Ext_eval (((@ (F,(fc . jc))) * ((g1 . j1) *' (g1 . j1))),a) by I0, D, H5
.= (fc . jc) * (Ext_eval (((g1 . j1) *' (g1 . j1)),a)) by H6, lem20
.= (fc . jc) * ((Ext_eval ((g1 . j1),a)) * (Ext_eval ((g1 . j1),a))) by H0, ALGNUM_1:20
.= (fc . jc) * ((fd . jd) * (Ext_eval ((g1 . j1),a))) by H3, B
.= f . j3 by H3, B ; :: thesis:

end;

hence g3 = f by B, C, D, FINSEQ_2:9; :: thesis:

end;

assume q is zero ; :: thesis:
then I1: ( len g3 = len g2 & q = 0_. F ) by D, UPROOTS:def 5;
for i being Element of dom g2
for r being Polynomial of F st r = g2 . i holds
g3 . i = Ext_eval (r,a) by D;
then Sum f = Ext_eval (q,a) by H2, D, lem
.= 0. E by I1, ALGNUM_1:13 ;
hence contradiction by A; :: thesis:

end;

then reconsider q = Sum g2 as non zero Polynomial of F ;
Ext_eval (((1_. F) + q),a) = 0. E

for i being Element of dom g2
for r being Polynomial of F st r = g2 . i holds
g3 . i = Ext_eval (r,a) by D;
then Ext_eval (q,a) = - (1. E) by A, H2, D, lem;
hence Ext_eval (((1_. F) + q),a) = (Ext_eval ((1_. F),a)) + (- (1. E)) by H0, ALGNUM_1:15
.= (1. E) + (- (1. E)) by H0, ALGNUM_1:14
.= 0. E by RLVECT_1:5 ;
:: thesis:

end;

then consider h being Polynomial of F such that
F: (MinPoly (a,F)) *' h = (1_. F) + q by H1, FIELD_6:53, RING_4:1;
ex h1 being monic non constant Element of the carrier of (Polynom-Ring F) st
( h1 divides h & h1 is irreducible & deg h1 is odd & deg h1 < (2 * k) + 1 )

per cases ;

suppose F1: h <> 0_. F ; :: thesis:

reconsider h = h as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
G1: ( not h is zero & not MinPoly (a,F) is zero ) by F1, UPROOTS:def 5;
F2: (deg (MinPoly (a,F))) + (deg h) = deg ((1_. F) + q) by F, F1, HURWITZ:23;
then G2: deg ((1_. F) + q) >= (2 * k) + 1 by A1, AS3, G1, NAT_1:11;
reconsider p = (1_. F) + q as non zero Polynomial of F by G1, F;
F4: deg q is even

let j2 be Element of dom g2; :: thesis:
let r be Polynomial of F; :: thesis:
assume O1: r = g2 . j2 ; :: thesis:
reconsider j1 = j2 as Element of dom g1 by I0;
consider jc being Element of dom fc such that
O2: ( jc = j1 & g2 . j1 = (@ (F,(fc . jc))) * ((g1 . j1) *' (g1 . j1)) ) by C;
consider jd being Element of dom fd such that
O3: ( jd = jc & fc . jc in P & fc . jc <> 0. E & f . jc = (fc . jc) * ((fd . jd) * (fd . jd)) ) by U;
O4: g1 . j1 <> 0_. F by B;
reconsider r1 = g1 . j1 as Polynomial of F ;
O8: fc . jc is F -membered by O3;
then O7: not @ (F,(fc . jc)) is zero by O3, H0, C0SP1:def 3;
then deg r = deg (r1 *' r1) by O2, O1, RING_5:4
.= (deg r1) + (deg r1) by O4, HURWITZ:23
.= 2 * (deg (g1 . j1)) ;
hence deg r is even ; :: thesis:
O5: LC r = (@ (F,(fc . jc))) * (LC (r1 *' r1)) by O1, O2, RING_5:5
.= (@ (F,(fc . jc))) * ((LC r1) * (LC r1)) by NIVEN:46 ;
not r1 is zero by B;
then ( (LC r1) ^2 in P & not (LC r1) ^2 in {(0. F)} ) by REALALG1:23, TARSKI:def 1;
then O6: (LC r1) ^2 in P ^+ by XBOOLE_0:def 5;
( @ (F,(fc . jc)) = fc . jc & not @ (F,(fc . jc)) in {(0. F)} ) by O7, O8, TARSKI:def 1;
then @ (F,(fc . jc)) in P ^+ by O3, XBOOLE_0:def 5;
then LC r in P ^+ by O5, O6, REALALG1:def 5;
hence LC r in P by XBOOLE_0:def 5; :: thesis:

end;

hence deg q is even by lem23; :: thesis:

end;

F5: deg p = deg q

assume deg q = deg (1_. F) ; :: thesis:
then deg p <= max ((deg (1_. F)),(deg (1_. F))) by HURWITZ:22;
hence contradiction by G2, RATFUNC1:def 2; :: thesis:

end;

then I2: deg p = max ((deg (1_. F)),(deg q)) by HURWITZ:21;
then max ((deg (1_. F)),(deg q)) <> deg (1_. F) by F2, A1, G1, RATFUNC1:def 2;
hence deg p = deg q by I2, XXREAL_0:16; :: thesis:

end;

then deg h is odd by A1, AS3, F2, F4;
then consider h1 being monic non constant Element of the carrier of (Polynom-Ring F) such that
F8: ( h1 divides h & h1 is irreducible & deg h1 is odd ) by lem21;
deg p <= (2 * ((2 * k) + 1)) - 2

0 + 1 <= k by AS2, INT_1:7;
then 2 * 1 <= 2 * k by XREAL_1:64;
then 2 + 1 <= (2 * k) + 1 by XREAL_1:6;
then 2 * 3 <= 2 * ((2 * k) + 1) by XREAL_1:64;
then 6 - 2 <= (2 * ((2 * k) + 1)) - 2 by XREAL_1:9;
then I: (2 * ((2 * k) + 1)) - 2 is Element of NAT by INT_1:3, XXREAL_0:2;

let j2 be Element of dom g2; :: thesis:
let r be Polynomial of F; :: thesis:
assume O1: r = g2 . j2 ; :: thesis:
reconsider j1 = j2 as Element of dom g1 by I0;
consider jc being Element of dom fc such that
O2: ( jc = j1 & g2 . j1 = (@ (F,(fc . jc))) * ((g1 . j1) *' (g1 . j1)) ) by C;
consider jd being Element of dom fd such that
O3: ( jd = jc & fc . jc in P & fc . jc <> 0. E & f . jc = (fc . jc) * ((fd . jd) * (fd . jd)) ) by U;
O4: g1 . j1 <> 0_. F by B;
reconsider r1 = g1 . j1 as Polynomial of F ;
fc . jc is F -membered by O3;
then O6: not @ (F,(fc . jc)) is zero by O3, H0, C0SP1:def 3;
deg (g1 . j1) < (2 * k) + 1 by B, AS3, A1;
then I3: ((deg (g1 . j1)) + 1) - 1 <= ((2 * k) + 1) - 1 by INT_1:7;
I5: deg r = deg (r1 *' r1) by O6, O1, O2, RING_5:4
.= (deg r1) + (deg r1) by O4, HURWITZ:23 ;
(deg r1) + (deg r1) <= (2 * k) + (2 * k) by I3, XREAL_1:7;
hence deg r <= (2 * ((2 * k) + 1)) - 2 by I5; :: thesis:

end;

hence deg p <= (2 * ((2 * k) + 1)) - 2 by F5, I, lem24; :: thesis:

end;

then F9: (deg p) - ((2 * k) + 1) <= ((2 * ((2 * k) + 1)) - 2) - ((2 * k) + 1) by XREAL_1:6;
deg h1 <= deg h by F8, G1, RING_5:13;
then deg h1 <= ((2 * k) + 1) - 2 by F9, F2, A1, AS3, XXREAL_0:2;
then (deg h1) + 0 < (((2 * k) + 1) - 2) + 2 by XREAL_1:8;
hence ex h1 being monic non constant Element of the carrier of (Polynom-Ring F) st
( h1 divides h & h1 is irreducible & deg h1 is odd & deg h1 < (2 * k) + 1 ) by F8; :: thesis:

end;

suppose h = 0_. F ; :: thesis:

then (X- (1. F)) *' (0_. F) = h ;
then A: X- (1. F) divides h by RING_4:1;
deg (X- (1. F)) = (2 * 0) + 1 by FIELD_5:def 1;
hence ex h1 being monic non constant Element of the carrier of (Polynom-Ring F) st
( h1 divides h & h1 is irreducible & deg h1 is odd & deg h1 < (2 * k) + 1 ) by A, AS2, XREAL_1:6; :: thesis:

end;

then consider h1 being monic non constant Element of the carrier of (Polynom-Ring F) such that
H: ( h1 divides h & h1 is irreducible & deg h1 is odd & deg h1 < (2 * k) + 1 ) ;
consider E2 being FieldExtension of F such that
J: h1 is_with_roots_in E2 by FIELD_5:30;
consider b being Element of E2 such that
J1: b is_a_root_of h1,E2 by J, FIELD_4:def 3;
K: Ext_eval (h1,b) = 0. E2 by J1, FIELD_4:def 2;
then reconsider b = b as F -algebraic Element of E2 by FIELD_6:43;
I3: F is Subring of E2 by FIELD_4:def 1;
I4: FAdj (F,{b}) is Subring of E2 by FIELD_5:12;
then 1. (FAdj (F,{b})) = 1. E2 by C0SP1:def 3;
then I5: - (1. (FAdj (F,{b}))) = - (1. E2) by I4, FIELD_6:17;
L: P extends_to FAdj (F,{b})

consider m being Integer such that
I1: deg h1 = (2 * m) + 1 by H, ABIAN:1;
m >= 0 by I1, INT_1:7;
then reconsider m = m as Element of NAT by INT_1:3;
I2: m < k

((2 * m) + 1) - 1 < ((2 * k) + 1) - 1 by H, I1, XREAL_1:9;
then (2 * m) - (2 * k) < (2 * k) - (2 * k) by XREAL_1:9;
then 2 * (m - k) < 0 ;
then m - k < 0 ;
then (m - k) + k < 0 + k by XREAL_1:6;
hence m < k ; :: thesis:

end;

h1 = MinPoly (b,F) by H, K, FIELD_6:52;
then deg ((FAdj (F,{b})),F) = deg h1 by FIELD_6:67;
hence P extends_to FAdj (F,{b}) by I1, I2, AS1; :: thesis:

end;

M: Ext_eval (q,b) = - (1. E2)

N: Ext_eval (h,b) = 0. E2

consider r being Polynomial of F such that
N1: h = h1 *' r by H, RING_4:1;
thus Ext_eval (h,b) = (Ext_eval (h1,b)) * (Ext_eval (r,b)) by N1, I3, ALGNUM_1:20
.= 0. E2 by K ; :: thesis:

end;

0. E2 = (Ext_eval ((MinPoly (a,F)),b)) * (Ext_eval (h,b)) by N
.= Ext_eval (((1_. F) + q),b) by F, I3, ALGNUM_1:20
.= (Ext_eval ((1_. F),b)) + (Ext_eval (q,b)) by I3, ALGNUM_1:15
.= (1. E2) + (Ext_eval (q,b)) by I3, ALGNUM_1:14 ;
then ((1. E2) + (Ext_eval (q,b))) - (1. E2) = - (1. E2) ;
hence - (1. E2) = ((1. E2) + (- (1. E2))) + (Ext_eval (q,b)) by RLVECT_1:def 3
.= (0. E2) + (Ext_eval (q,b)) by RLVECT_1:5
.= Ext_eval (q,b) ;
:: thesis:

end;

ex g4 being non empty FinSequence of E2 st
( len g4 = len g2 & ( for i being Element of dom g2 holds g4 . i = Ext_eval ((g2 . i),b) ) )

defpred S₂[ Nat, object ] means ex j being Element of dom g2 st
( j = $1 & $2 = Ext_eval ((g2 . j),b) );

let k be Nat; :: thesis:
assume k in Seg (len g2) ; :: thesis:
then reconsider j = k as Element of dom g2 by FINSEQ_1:def 3;
thus ex x being Element of E2 st S₂[k,x] :: thesis:

take Ext_eval ((g2 . j),b) ; :: thesis:
thus S₂[k, Ext_eval ((g2 . j),b)] ; :: thesis:

end;

consider p being FinSequence of E2 such that
M: ( dom p = Seg (len g2) & ( for k being Nat st k in Seg (len g2) holds
S₂[k,p . k] ) ) from FINSEQ_1:sch 5(N);
reconsider p = p as non empty FinSequence of E2 by M;
take p ; :: thesis:

let i be Element of dom g2; :: thesis:
reconsider k = i as Nat ;
k in dom g2 ;
then k in Seg (len g2) by FINSEQ_1:def 3;
then S₂[k,p . k] by M;
hence p . i = Ext_eval ((g2 . i),b) ; :: thesis:

end;

hence ( len p = len g2 & ( for i being Element of dom g2 holds p . i = Ext_eval ((g2 . i),b) ) ) by M, FINSEQ_1:def 3; :: thesis:

end;

then consider g4 being non empty FinSequence of E2 such that
N: ( len g4 = len g2 & ( for i being Element of dom g2 holds g4 . i = Ext_eval ((g2 . i),b) ) ) ;
I9: dom g4 = dom g2

dom g4 = Seg (len g2) by N, FINSEQ_1:def 3;
hence dom g4 = dom g2 by FINSEQ_1:def 3; :: thesis:

end;

P: rng g4 c= the carrier of (FAdj (F,{b}))

let j4 be object ; :: thesis:
assume j4 in rng g4 ; :: thesis:
then consider i being object such that
P1: ( i in dom g4 & g4 . i = j4 ) by FUNCT_1:def 3;
reconsider j1 = i as Element of dom g1 by P1, I0, I9;
consider jc being Element of dom fc such that
O2: ( jc = j1 & g2 . j1 = (@ (F,(fc . jc))) * ((g1 . j1) *' (g1 . j1)) ) by C;
consider jd being Element of dom fd such that
O3: ( jd = jc & fc . jc in P & fc . jc <> 0. E & f . jc = (fc . jc) * ((fd . jd) * (fd . jd)) ) by U;
set c = fc . jc;
set d = fd . jd;
reconsider c = fc . jc as F -membered Element of E by O3, FIELD_7:def 5;
F is Subfield of E2 by FIELD_4:7;
then the carrier of F c= the carrier of E2 by EC_PF_1:def 1;
then reconsider c1 = c as Element of E2 by O3;
reconsider c1 = c1 as F -membered Element of E2 by O3, FIELD_7:def 5;
P5: F is Subfield of FAdj (F,{b}) by FIELD_6:36;
then ( the carrier of F c= the carrier of (FAdj (F,{b})) & c1 in F ) by O3, EC_PF_1:def 1;
then reconsider c2 = c1 as Element of (FAdj (F,{b})) ;
F is Subfield of E by FIELD_4:7;
then ( 0. E = 0. F & 0. F = 0. (FAdj (F,{b})) & c <> 0. E ) by O3, P5, EC_PF_1:def 1;
then reconsider c2 = c2 as non zero Element of (FAdj (F,{b})) by STRUCT_0:def 12;
( b in {b} & {b} is Subset of (FAdj (F,{b})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider b1 = b as Element of (FAdj (F,{b})) ;
reconsider r = g1 . j1 as Polynomial of F ;
P4: g4 . i = Ext_eval (((@ (F,c)) * (r *' r)),b) by P1, I9, O2, N
.= c1 * (Ext_eval ((r *' r),b)) by lem20
.= c1 * ((Ext_eval (r,b)) * (Ext_eval (r,b))) by I3, ALGNUM_1:20 ;
E2 is FAdj (F,{b}) -extending by I4, FIELD_4:def 1;
then Ext_eval (r,b) = Ext_eval (r,b1) by FIELD_6:11;
then (Ext_eval (r,b)) * (Ext_eval (r,b)) = (Ext_eval (r,b1)) * (Ext_eval (r,b1)) by I4, FIELD_6:16;
then c2 * ((Ext_eval (r,b1)) ^2) = c1 * ((Ext_eval (r,b)) ^2) by I4, FIELD_6:16;
hence j4 in the carrier of (FAdj (F,{b})) by P1, P4; :: thesis:

end;

hence rng g4 c= the carrier of (FAdj (F,{b})) ; :: thesis:

end;

reconsider g5 = g4 as non empty FinSequence of (FAdj (F,{b})) by P, FINSEQ_1:def 4;

let i be Element of NAT ; :: thesis:
assume P1: i in dom g4 ; :: thesis:
then reconsider j1 = i as Element of dom g1 by I0, I9;
consider jc being Element of dom fc such that
O2: ( jc = j1 & g2 . j1 = (@ (F,(fc . jc))) * ((g1 . j1) *' (g1 . j1)) ) by C;
consider jd being Element of dom fd such that
O3: ( jd = jc & fc . jc in P & fc . jc <> 0. E & f . jc = (fc . jc) * ((fd . jd) * (fd . jd)) ) by U;
set c = fc . jc;
set d = fd . jd;
reconsider c = fc . jc as F -membered Element of E by O3, FIELD_7:def 5;
F is Subfield of E2 by FIELD_4:7;
then the carrier of F c= the carrier of E2 by EC_PF_1:def 1;
then reconsider c1 = c as Element of E2 by O3;
reconsider c1 = c1 as F -membered Element of E2 by O3, FIELD_7:def 5;
P5: F is Subfield of FAdj (F,{b}) by FIELD_6:36;
then ( the carrier of F c= the carrier of (FAdj (F,{b})) & c1 in F ) by O3, EC_PF_1:def 1;
then reconsider c2 = c1 as Element of (FAdj (F,{b})) ;
F is Subfield of E by FIELD_4:7;
then ( 0. E = 0. F & 0. F = 0. (FAdj (F,{b})) & c <> 0. E ) by O3, P5, EC_PF_1:def 1;
then reconsider c2 = c2 as non zero Element of (FAdj (F,{b})) by STRUCT_0:def 12;
( b in {b} & {b} is Subset of (FAdj (F,{b})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider b1 = b as Element of (FAdj (F,{b})) ;
reconsider r = g1 . j1 as Polynomial of F ;
P4: g4 . i = Ext_eval (((@ (F,c)) * (r *' r)),b) by P1, I9, O2, N
.= c1 * (Ext_eval ((r *' r),b)) by lem20
.= c1 * ((Ext_eval (r,b)) * (Ext_eval (r,b))) by I3, ALGNUM_1:20 ;
E2 is FAdj (F,{b}) -extending by I4, FIELD_4:def 1;
then Ext_eval (r,b) = Ext_eval (r,b1) by FIELD_6:11;
then (Ext_eval (r,b)) * (Ext_eval (r,b)) = (Ext_eval (r,b1)) * (Ext_eval (r,b1)) by I4, FIELD_6:16;
then c2 * ((Ext_eval (r,b1)) ^2) = c1 * ((Ext_eval (r,b)) ^2) by I4, FIELD_6:16;
hence ex c being non zero Element of (FAdj (F,{b})) ex d being Element of (FAdj (F,{b})) st
( c in P & g4 . i = c * (d ^2) ) by P4, O3; :: thesis:

end;

then reconsider g5 = g5 as non empty P -quadratic FinSequence of (FAdj (F,{b})) by dq;
for i being Element of dom g2
for r being Polynomial of F st r = g2 . i holds
g4 . i = Ext_eval (r,b) by N;
then - (1. (FAdj (F,{b}))) = Sum g4 by M, I5, N, lem
.= Sum g5 by I4, FIELD_4:2 ;
then - (1. (FAdj (F,{b}))) in QS ((FAdj (F,{b})),P) ;
hence contradiction by L, lemoe2, lemoe4; :: thesis:

end;

hence P extends_to E1 by lemoe2, lemoe4; :: thesis:

end;

hence S₁[k] ; :: thesis:

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(IS);
reconsider n = deg (E1,F) as odd Nat by AS;
consider k being Integer such that
H: n = (2 * k) + 1 by ABIAN:1;