let p be Polynomial of F_Complex; :: thesis: ( len p > 1 implies p is with_roots )
assume A1: len p > 1 ; :: thesis: p is with_roots
then A2: len p >= 1 + 1 by NAT_1:13;

per cases ( len p > 2 or len p = 2 ) by A2, XXREAL_0:1;

suppose len p > 2 ; :: thesis: p is with_roots

then consider z0 being Element of F_Complex such that
A3: for z being Element of F_Complex holds |.(eval (p,z)).| >= |.(eval (p,z0)).| by Th73;
set q = Subst (p,<%z0,(1_ F_Complex)%>);
defpred S₁[ Nat] means ( $1 >= 1 & (Subst (p,<%z0,(1_ F_Complex)%>)) . $1 <> 0. F_Complex );
len <%z0,(1_ F_Complex)%> = 2 by Th40;
then A4: len (Subst (p,<%z0,(1_ F_Complex)%>)) = (((2 * (len p)) - (len p)) - 2) + 2 by A1, Th52
.= len p ;
A5: ex k being Nat st S₁[k]

proof

(len (Subst (p,<%z0,(1_ F_Complex)%>))) - 1 = (len (Subst (p,<%z0,(1_ F_Complex)%>))) -' 1 by A1, A4, XREAL_0:def 2;
then reconsider k = (len (Subst (p,<%z0,(1_ F_Complex)%>))) - 1 as Element of NAT ;
take k ; :: thesis: S₁[k]
len (Subst (p,<%z0,(1_ F_Complex)%>)) >= 1 + 1 by A1, A4, NAT_1:13;
hence k >= 1 by XREAL_1:19; :: thesis: (Subst (p,<%z0,(1_ F_Complex)%>)) . k <> 0. F_Complex
len (Subst (p,<%z0,(1_ F_Complex)%>)) = k + 1 ;
hence (Subst (p,<%z0,(1_ F_Complex)%>)) . k <> 0. F_Complex by ALGSEQ_1:10; :: thesis: verum

end;

consider k being Nat such that
A6: S₁[k] and
A7: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A5);
A8: k + 1 > 1 by A6, NAT_1:13;
reconsider k1 = k as non zero Element of NAT by A6, ORDINAL1:def 12;
set sq = the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1));
deffunc H₁( Nat) -> Element of the carrier of F_Complex = ((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k1 + $1),NAT))) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(In ((k1 + $1),NAT))));
consider F2 being FinSequence of the carrier of F_Complex such that
A9: len F2 = (len (Subst (p,<%z0,(1_ F_Complex)%>))) -' (k1 + 1) and
A10: for n being Nat st n in dom F2 holds
F2 . n = H₁(n) from FINSEQ_2:sch 1();
k1 < len (Subst (p,<%z0,(1_ F_Complex)%>)) by A6, ALGSEQ_1:8;
then A11: (k + 1) + 0 <= len (Subst (p,<%z0,(1_ F_Complex)%>)) by NAT_1:13;
then (len (Subst (p,<%z0,(1_ F_Complex)%>))) - (k + 1) >= 0 by XREAL_1:19;
then A12: len F2 = (len (Subst (p,<%z0,(1_ F_Complex)%>))) - (k + 1) by A9, XREAL_0:def 2;
A13: eval (p,z0) = eval (p,(z0 + (0. F_Complex))) by RLVECT_1:def 4
.= eval (p,(eval (<%z0,(1_ F_Complex)%>,(0. F_Complex)))) by Th47
.= eval ((Subst (p,<%z0,(1_ F_Complex)%>)),(0. F_Complex)) by Th53 ;

A14: now :: thesis: for z being Element of F_Complex holds |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).|

let z be Element of F_Complex; :: thesis: |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).|
eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z) = eval (p,(eval (<%z0,(1_ F_Complex)%>,z))) by Th53
.= eval (p,(z0 + z)) by Th47 ;
then |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.(eval (p,z0)).| by A3;
hence |.(eval ((Subst (p,<%z0,(1_ F_Complex)%>)),z)).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A13, Th31; :: thesis: verum

end;

now :: thesis: for c being Real st 0 < c & c < 1 holds
c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).|

let c be Real; :: thesis: ( 0 < c & c < 1 implies c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| )
assume that
A15: 0 < c and
A16: c < 1 ; :: thesis: c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).|
set z1 = [**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1));
consider F1 being FinSequence of the carrier of F_Complex such that
A17: eval ((Subst (p,<%z0,(1_ F_Complex)%>)),([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)))) = Sum F1 and
A18: len F1 = len (Subst (p,<%z0,(1_ F_Complex)%>)) and
A19: for n being Element of NAT st n in dom F1 holds
F1 . n = ((Subst (p,<%z0,(1_ F_Complex)%>)) . (n -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(n -' 1))) by POLYNOM4:def 2;
A20: dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) = dom (F1 /^ (k + 1)) by POLYNOM1:def 2;
A21: k1 < len F1 by A6, A18, ALGSEQ_1:8;
reconsider FF = F1 | k1 as FinSequence of the carrier of F_Complex ;
1 in Seg k by A6, FINSEQ_1:1;
then 1 in Seg (len (F1 | k)) by A21, FINSEQ_1:59;
then A22: 1 in dom FF by FINSEQ_1:def 3;
A23: dom FF c= dom F1 by FINSEQ_5:18;

now :: thesis: for i being Element of NAT st i in dom FF & i <> 1 holds
FF /. i = 0. F_Complex

let i be Element of NAT ; :: thesis: ( i in dom FF & i <> 1 implies FF /. i = 0. F_Complex )
assume that
A24: i in dom FF and
A25: i <> 1 ; :: thesis: FF /. i = 0. F_Complex
A26: 0 + 1 <= i by A24, FINSEQ_3:25;
then i > 1 by A25, XXREAL_0:1;
then i >= 1 + 1 by NAT_1:13;
then i - 1 >= (1 + 1) - 1 by XREAL_1:9;
then A27: i -' 1 >= 1 by XREAL_0:def 2;
i <= len (F1 | k) by A24, FINSEQ_3:25;
then i <= k by A21, FINSEQ_1:59;
then i < k + 1 by NAT_1:13;
then A28: i - 1 < k by XREAL_1:19;
i - 1 >= 0 by A26;
then A29: i -' 1 < k by A28, XREAL_0:def 2;
thus FF /. i = F1 /. i by A24, FINSEQ_4:70
.= F1 . i by A23, A24, PARTFUN1:def 6
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (i -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(i -' 1))) by A19, A23, A24
.= (0. F_Complex) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(i -' 1))) by A7, A27, A29
.= 0. F_Complex ; :: thesis: verum

end;

then A30: Sum FF = FF /. 1 by A22, POLYNOM2:3
.= F1 /. 1 by A22, FINSEQ_4:70
.= F1 . 1 by A22, A23, PARTFUN1:def 6
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (1 -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(1 -' 1))) by A19, A22, A23
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(1 -' 1))) by XREAL_1:232
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),0)) by XREAL_1:232
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * (1_ F_Complex) by GROUP_1:def 7
.= (Subst (p,<%z0,(1_ F_Complex)%>)) . 0 ;
k + 1 in Seg (len F1) by A8, A11, A18, FINSEQ_1:1;
then A31: k + 1 in dom F1 by FINSEQ_1:def 3;
then A32: F1 . (k + 1) = F1 /. (k + 1) by PARTFUN1:def 6;
set gc = (Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**];
A33: c to_power (k + 1) > 0 by A15, POWER:34;
then A34: Sum (F1 /^ (k + 1)) = ([**(c to_power (k + 1)),0**] * (Sum (F1 /^ (k + 1)))) / [**(c to_power (k + 1)),0**] by COMPLFLD:7, COMPLFLD:30
.= [**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]) ;
A35: F1 /. (k + 1) = F1 . (k + 1) by A31, PARTFUN1:def 6
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . ((k + 1) -' 1)) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),((k + 1) -' 1))) by A19, A31
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),((k + 1) -' 1))) by NAT_D:34
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),k1)) by NAT_D:34
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (((power F_Complex) . ([**c,0**],k1)) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),k1))) by GROUP_1:52
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (((power F_Complex) . ([**c,0**],k1)) * (- (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)))) by COMPLFLD:def 2
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (- (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)))) * ((power F_Complex) . ([**c,0**],k1))
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * ((- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))) * ((power F_Complex) . ([**c,0**],k1)) by A6, COMPLFLD:42
.= ((((Subst (p,<%z0,(1_ F_Complex)%>)) . k1) * (- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0))) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)) * ((power F_Complex) . ([**c,0**],k1))
.= (- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) * ((power F_Complex) . ([**c,0**],k1)) by A6, COMPLFLD:30
.= (- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) * [**(c to_power k),0**] by A15, HAHNBAN1:29 ;
A36: |.((((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])) + ([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]))).| <= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])).| + |.([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])).| by COMPLFLD:62;
F1 = ((F1 | ((k + 1) -' 1)) ^ <*(F1 . (k + 1))*>) ^ (F1 /^ (k + 1)) by A8, A11, A18, POLYNOM4:1;
then Sum F1 = (Sum ((F1 | ((k + 1) -' 1)) ^ <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by A32, RLVECT_1:41
.= ((Sum (F1 | ((k + 1) -' 1))) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by RLVECT_1:41
.= ((Sum (F1 | k)) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by NAT_D:34
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) + ((- ((Subst (p,<%z0,(1_ F_Complex)%>)) . 0)) * [**(c to_power k),0**])) + (Sum (F1 /^ (k + 1))) by A30, A35, RLVECT_1:44
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) + (- (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * [**(c to_power k),0**]))) + (Sum (F1 /^ (k + 1))) by VECTSP_1:9
.= ((((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * (1_ F_Complex)) - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * [**(c to_power k),0**])) + (Sum (F1 /^ (k + 1)))
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])) + ([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])) by A34, VECTSP_1:11 ;
then |.((((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])) + ([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]))).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A14, A17;
then |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) * ((1_ F_Complex) - [**(c to_power k),0**])).| + |.([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A36, XXREAL_0:2;
then (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * |.((1_ F_Complex) - [**(c to_power k),0**]).|) + |.([**(c to_power (k + 1)),0**] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**])).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by COMPLFLD:71;
then A37: (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * |.((1_ F_Complex) - [**(c to_power k),0**]).|) + (|.[**(c to_power (k + 1)),0**].| * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by COMPLFLD:71;
0 + (c to_power k1) <= 1 by A15, A16, TBSP_1:2;
then A38: 1 - (c to_power k) >= 0 by XREAL_1:19;
A39: c to_power k > 0 by A15, POWER:34;
A40: len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| = len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) by Def2
.= len (F1 /^ (k + 1)) by A20, FINSEQ_3:29
.= (len F1) - (k + 1) by A11, A18, RFINSEQ:def 1
.= len |.F2.| by A12, A18, Def2 ;

now :: thesis: for i being Element of NAT st i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| holds
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i

let i be Element of NAT ; :: thesis: ( i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| implies |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i )
A41: ((k + 1) + i) -' 1 = ((k + i) + 1) - 1 by XREAL_0:def 2
.= k + i ;
assume i in dom |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| ; :: thesis: |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i
then A43: i in Seg (len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).|) by FINSEQ_1:def 3;
then i <= len |.F2.| by A40, FINSEQ_1:1;
then i <= (len F1) - (k + 1) by A12, A18, Def2;
then ( (k + i) + 1 >= 0 + 1 & (k + 1) + i <= len F1 ) by XREAL_1:6, XREAL_1:19;
then A44: (k + 1) + i in dom F1 by FINSEQ_3:25;
i >= 0 + 1 by A43, FINSEQ_1:1;
then A45: i - 1 >= 0 ;
c to_power (i -' 1) <= 1 by A15, A16, TBSP_1:2;
then A46: c to_power (i - 1) <= 1 by A45, XREAL_0:def 2;
A47: c to_power (k + i) > 0 by A15, POWER:34;
A48: (k + i) - (k + 1) = i - 1 ;
i in Seg (len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] "))) by A43, Def2;
then A49: i in dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) by FINSEQ_1:def 3;
then A50: (F1 /^ (k + 1)) /. i = (F1 /^ (k + 1)) . i by A20, PARTFUN1:def 6
.= F1 . ((k + 1) + i) by A11, A18, A20, A49, RFINSEQ:def 1
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((((k + 1) + i) -' 1),NAT))) * ((power F_Complex) . (([**c,0**] * the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1))),(((k + 1) + i) -' 1))) by A19, A44
.= ((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * ((power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i))) * (power ([**c,0**],(k + i)))) by A41, GROUP_1:52
.= (((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))) * (power ([**c,0**],(k + i))) ;
A51: len F2 = len |.F2.| by Def2;
A53: |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i = |.(((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) . i).| by A49, Def2
.= |.(((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) /. i).| by A49, PARTFUN1:def 6
.= |.(((F1 /^ (k + 1)) /. i) * ([**(c to_power (k + 1)),0**] ")).| by A20, A49, POLYNOM1:def 2
.= |.((F1 /^ (k + 1)) /. i).| * |.([**(c to_power (k + 1)),0**] ").| by COMPLFLD:71
.= |.((((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))) * (power ([**c,0**],(k + i)))).| * (|.(c to_power (k + 1)).| ") by A33, A50, COMPLFLD:7, COMPLFLD:72
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * |.(power ([**c,0**],(k + i))).|) * (|.(c to_power (k + 1)).| ") by COMPLFLD:71
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * |.[**(c to_power (k + i)),0**].|) * (|.(c to_power (k + 1)).| ") by A15, HAHNBAN1:29
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * (c to_power (k + i))) * (|.(c to_power (k + 1)).| ") by A47, ABSVALUE:def 1
.= (|.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * (c to_power (k + i))) * ((c to_power (In ((k + 1),NAT))) ") by A33, ABSVALUE:def 1
.= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * ((c to_power (k + i)) * ((c to_power (k + 1)) "))
.= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * ((c to_power (k + i)) / (c to_power (k + 1)))
.= |.(((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i)))).| * (c to_power (i - 1)) by A15, A48, POWER:29 ;
A54: i in dom F2 by A40, A43, A51, FINSEQ_1:def 3;
((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * (power ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(k + i))) = ((Subst (p,<%z0,(1_ F_Complex)%>)) . (In ((k + i),NAT))) * ((power F_Complex) . ( the CRoot of k1, - (((Subst (p,<%z0,(1_ F_Complex)%>)) . 0) / ((Subst (p,<%z0,(1_ F_Complex)%>)) . k1)),(In ((k + i),NAT))))
.= H₁(i)
.= F2 . i by A54, A10 ;
then |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.(F2 . i).| by A46, A53, COMPLEX1:46, XREAL_1:153;
hence |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| . i <= |.F2.| . i by A54, Def2; :: thesis: verum

end;

then A55: Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| <= Sum |.F2.| by A40, INTEGRA5:3;
|.((1_ F_Complex) - [**(c to_power k),0**]).| = |.([**1,0**] - [**(c to_power k),0**]).| by COMPLEX1:def 4, COMPLFLD:8
.= |.[**(1 - (c to_power k1)),(0 - 0)**].| by Th6
.= 1 - (c to_power k) by A38, ABSVALUE:def 1 ;
then |.[**(c to_power (k + 1)),0**].| * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * 1) - (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * (1 - (c to_power k))) by A37, XREAL_1:20;
then (c to_power (k + 1)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * (c to_power k) by A33, ABSVALUE:def 1;
then ((c to_power (k + 1)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).|) / (c to_power k) >= (|.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| * (c to_power k)) / (c to_power k) by A39, XREAL_1:72;
then ((c to_power (k + 1)) / (c to_power k)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A39, XCMPLX_1:89;
then (c to_power ((k + 1) - k)) * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A15, POWER:29;
then A56: c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by POWER:25;
(Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**] = (Sum (F1 /^ (k + 1))) * ([**(c to_power (k + 1)),0**] ")
.= Sum ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")) by POLYNOM1:13 ;
then |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| <= Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0**] ")).| by Th14;
then |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| <= Sum |.F2.| by A55, XXREAL_0:2;
then c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0**]).| <= c * (Sum |.F2.|) by A15, XREAL_1:64;
hence c * (Sum |.F2.|) >= |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| by A56, XXREAL_0:2; :: thesis: verum

end;

then |.((Subst (p,<%z0,(1_ F_Complex)%>)) . 0).| <= 0 by Lm1;
then A57: (Subst (p,<%z0,(1_ F_Complex)%>)) . 0 = 0. F_Complex by COMPLFLD:59;
ex x being Element of F_Complex st x is_a_root_of p

proof

take z0 ; :: thesis: z0 is_a_root_of p
eval (p,z0) = 0. F_Complex by A13, A57, Th31;
hence z0 is_a_root_of p ; :: thesis: verum

end;

hence p is with_roots ; :: thesis: verum

end;

suppose A58: len p = 2 ; :: thesis: p is with_roots

set np = NormPolynomial p;
A59: (len p) -' 1 = 2 - 1 by A58, XREAL_0:def 2;
A60: len (NormPolynomial p) = len p by A58, Th57;

A61: now :: thesis: for k being Nat st k < len (NormPolynomial p) holds
(NormPolynomial p) . k = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . k

let k be Nat; :: thesis: ( k < len (NormPolynomial p) implies (NormPolynomial p) . b₁ = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b₁ )
assume A62: k < len (NormPolynomial p) ; :: thesis: (NormPolynomial p) . b₁ = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b₁

per cases ( k = 0 or k = 1 ) by A58, A60, A62, NAT_1:23;

suppose k = 0 ; :: thesis: (NormPolynomial p) . b₁ = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b₁

hence (NormPolynomial p) . k = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . k by Th38; :: thesis: verum

end;

suppose A63: k = 1 ; :: thesis: (NormPolynomial p) . b₁ = <%((NormPolynomial p) . 0),(1_ F_Complex)%> . b₁

hence (NormPolynomial p) . k = 1_ F_Complex by A58, A59, Th56
.= <%((NormPolynomial p) . 0),(1_ F_Complex)%> . k by A63, Th38 ;
:: thesis: verum

end;

end;

end;

len <%((NormPolynomial p) . 0),(1_ F_Complex)%> = 2 by Th40;
then A64: NormPolynomial p = <%((NormPolynomial p) . 0),(1_ F_Complex)%> by A58, A61, Th57, ALGSEQ_1:12;
ex x being Element of F_Complex st x is_a_root_of NormPolynomial p

proof

take z0 = - ((NormPolynomial p) . 0); :: thesis: z0 is_a_root_of NormPolynomial p
eval ((NormPolynomial p),z0) = ((NormPolynomial p) . 0) + z0 by A64, Th47
.= 0. F_Complex by RLVECT_1:5 ;
hence z0 is_a_root_of NormPolynomial p ; :: thesis: verum

end;

then NormPolynomial p is with_roots ;
hence p is with_roots by A58, Th60; :: thesis: verum

end;

end;