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 Th74;
set q = Subst p,<%z0,(1_ F_Complex )%>;
A4: eval p,z0 = eval p,(z0 + (0. F_Complex )) by RLVECT_1:def 7
.= eval p,(eval <%z0,(1_ F_Complex )%>,(0. F_Complex )) by Th48
.= eval (Subst p,<%z0,(1_ F_Complex )%>),(0. F_Complex ) by Th54 ;

A5: now

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 Th54
.= eval p,(z0 + z) by Th48 ;
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 A4, Th32; :: thesis: verum

end;

len <%z0,(1_ F_Complex )%> = 2 by Th41;
then A6: len (Subst p,<%z0,(1_ F_Complex )%>) = (((2 * (len p)) - (len p)) - 2) + 2 by A1, Th53
.= len p ;
defpred S₁[ Nat] means ( $1 >= 1 & (Subst p,<%z0,(1_ F_Complex )%>) . $1 <> 0. F_Complex );
A7: ex k being Nat st S₁[k]

proof

(len (Subst p,<%z0,(1_ F_Complex )%>)) - 1 >= 1 - 1 by A1, A6, XREAL_1:11;
then (len (Subst p,<%z0,(1_ F_Complex )%>)) - 1 = (len (Subst p,<%z0,(1_ F_Complex )%>)) -' 1 by 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, A6, NAT_1:13;
hence k >= 1 by XREAL_1:21; :: 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:25; :: thesis: verum

end;

consider k being Nat such that
A8: S₁[k] and
A9: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A7);
A10: k + 1 > 1 by A8, NAT_1:13;
reconsider k1 = k as non empty Element of NAT by A8, ORDINAL1:def 13;
k1 < len (Subst p,<%z0,(1_ F_Complex )%>) by A8, ALGSEQ_1:22;
then A11: (k + 1) + 0 <= len (Subst p,<%z0,(1_ F_Complex )%>) by NAT_1:13;
consider sq being 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 )%>) . (k1 + $1)) * ((power F_Complex ) . sq,(k1 + $1));
consider F2 being FinSequence of the carrier of F_Complex such that
A12: len F2 = (len (Subst p,<%z0,(1_ F_Complex )%>)) -' (k1 + 1) and
A13: for n being Nat st n in dom F2 holds
F2 . n = H₁(n) from FINSEQ_2:sch 1();
(len (Subst p,<%z0,(1_ F_Complex )%>)) - (k + 1) >= 0 by A11, XREAL_1:21;
then A15: len F2 = (len (Subst p,<%z0,(1_ F_Complex )%>)) - (k + 1) by A12, XREAL_0:def 2;
A16: for n being Element of NAT st n in dom F2 holds
F2 . n = ((Subst p,<%z0,(1_ F_Complex )%>) . (k + n)) * ((power F_Complex ) . sq,(k + n)) by A13;

now

let c be Real; :: thesis: ( 0 < c & c < 1 implies c * (Sum |.F2.|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| )
assume A17: ( 0 < c & c < 1 ) ; :: thesis: c * (Sum |.F2.|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).|
set z1 = [**c,0 **] * sq;
consider F1 being FinSequence of the carrier of F_Complex such that
A18: eval (Subst p,<%z0,(1_ F_Complex )%>),([**c,0 **] * sq) = Sum F1 and
A19: len F1 = len (Subst p,<%z0,(1_ F_Complex )%>) and
A20: 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 **] * sq),(n -' 1)) by POLYNOM4:def 2;
k + 1 in Seg (len F1) by A10, A11, A19, FINSEQ_1:3;
then A21: k + 1 in dom F1 by FINSEQ_1:def 3;
then A22: F1 . (k + 1) = F1 /. (k + 1) by PARTFUN1:def 8;
A23: k1 < len F1 by A8, A19, ALGSEQ_1:22;
1 in Seg k by A8, FINSEQ_1:3;
then 1 in Seg (len (F1 | k)) by A23, FINSEQ_1:80;
then A24: 1 in dom (F1 | k) by FINSEQ_1:def 3;
A25: dom (F1 | k) c= dom F1 by FINSEQ_5:20;

now

let i be Element of NAT ; :: thesis: ( i in dom (F1 | k) & i <> 1 implies (F1 | k1) /. i = 0. F_Complex )
assume that
A26: i in dom (F1 | k) and
A27: i <> 1 ; :: thesis: (F1 | k1) /. i = 0. F_Complex
A28: ( 0 + 1 <= i & i <= len (F1 | k) ) by A26, FINSEQ_3:27;
then A29: i - 1 >= 0 by XREAL_1:21;
i > 1 by A27, A28, XXREAL_0:1;
then i >= 1 + 1 by NAT_1:13;
then i - 1 >= (1 + 1) - 1 by XREAL_1:11;
then A30: i -' 1 >= 1 by XREAL_0:def 2;
i <= k by A23, A28, FINSEQ_1:80;
then i < k + 1 by NAT_1:13;
then i - 1 < k by XREAL_1:21;
then A31: i -' 1 < k by A29, XREAL_0:def 2;
thus (F1 | k1) /. i = F1 /. i by A26, FINSEQ_4:85
.= F1 . i by A25, A26, PARTFUN1:def 8
.= ((Subst p,<%z0,(1_ F_Complex )%>) . (i -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(i -' 1)) by A20, A25, A26
.= (0. F_Complex ) * ((power F_Complex ) . ([**c,0 **] * sq),(i -' 1)) by A9, A30, A31
.= 0. F_Complex by VECTSP_1:39 ; :: thesis: verum

end;

then A32: Sum (F1 | k) = (F1 | k1) /. 1 by A24, POLYNOM2:5
.= F1 /. 1 by A24, FINSEQ_4:85
.= F1 . 1 by A24, A25, PARTFUN1:def 8
.= ((Subst p,<%z0,(1_ F_Complex )%>) . (1 -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(1 -' 1)) by A20, A24, A25
.= ((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((power F_Complex ) . ([**c,0 **] * sq),(1 -' 1)) by XREAL_1:234
.= ((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * ((power F_Complex ) . ([**c,0 **] * sq),0 ) by XREAL_1:234
.= ((Subst p,<%z0,(1_ F_Complex )%>) . 0 ) * (1_ F_Complex ) by GROUP_1:def 8
.= (Subst p,<%z0,(1_ F_Complex )%>) . 0 by GROUP_1:def 5 ;
A33: F1 /. (k + 1) = F1 . (k + 1) by A21, PARTFUN1:def 8
.= ((Subst p,<%z0,(1_ F_Complex )%>) . ((k + 1) -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),((k + 1) -' 1)) by A20, A21
.= ((Subst p,<%z0,(1_ F_Complex )%>) . k1) * ((power F_Complex ) . ([**c,0 **] * sq),((k + 1) -' 1)) by NAT_D:34
.= ((Subst p,<%z0,(1_ F_Complex )%>) . k1) * ((power F_Complex ) . ([**c,0 **] * sq),k1) by NAT_D:34
.= ((Subst p,<%z0,(1_ F_Complex )%>) . k1) * (((power F_Complex ) . [**c,0 **],k1) * ((power F_Complex ) . sq,k1)) by GROUP_1:100
.= ((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 A8, COMPLFLD:78
.= ((((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 A8, COMPLFLD:64
.= (- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 )) * ((power F_Complex ) . [**c,0 **],k1) by A8, COMPLFLD:66
.= (- ((Subst p,<%z0,(1_ F_Complex )%>) . 0 )) * [**(c to_power k),0 **] by A17, HAHNBAN1:37 ;
set gc = (Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **];
A34: c to_power (k + 1) > 0 by A17, POWER:39;
A35: c to_power k > 0 by A17, POWER:39;
0 + (c to_power k1) <= 1 by A17, TBSP_1:2;
then A36: 1 - (c to_power k) >= 0 by XREAL_1:21;
A37: Sum (F1 /^ (k + 1)) = ([**(c to_power (k + 1)),0 **] * (Sum (F1 /^ (k + 1)))) / [**(c to_power (k + 1)),0 **] by A34, COMPLFLD:9, COMPLFLD:66
.= [**(c to_power (k + 1)),0 **] * ((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]) by A34, COMPLFLD:9, COMPLFLD:64 ;
F1 = ((F1 | ((k + 1) -' 1)) ^ <*(F1 . (k + 1))*>) ^ (F1 /^ (k + 1)) by A10, A11, A19, POLYNOM4:3;
then Sum F1 = (Sum ((F1 | ((k + 1) -' 1)) ^ <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by A22, RLVECT_1:58
.= ((Sum (F1 | ((k + 1) -' 1))) + (Sum <*(F1 /. (k + 1))*>)) + (Sum (F1 /^ (k + 1))) by RLVECT_1:58
.= ((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 A32, A33, RLVECT_1:61
.= (((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:41
.= ((((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))) by VECTSP_1:def 13
.= (((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 A37, VECTSP_1:43 ;
then A38: |.((((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 A5, A18;
A39: |.((1_ F_Complex ) - [**(c to_power k),0 **]).| = |.([**1,0 **] - [**(c to_power k),0 **]).| by COMPLEX1:def 7, COMPLFLD:10
.= |.[**(1 - (c to_power k1)),(0 - 0 )**].| by Th6
.= 1 - (c to_power k) by A36, ABSVALUE:def 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 **]))).| <= |.(((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:100;
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 A38, 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:109;
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:109;
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 A39, XREAL_1:22;
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 A34, 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 A35, XREAL_1:74;
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 ).| by A35, XCMPLX_1:90;
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 ).| ;
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 A17, POWER:34;
then A40: c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| by POWER:30;
(Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **] = (Sum (F1 /^ (k + 1))) * ([**(c to_power (k + 1)),0 **] " ) by VECTSP_1:def 23
.= Sum ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) by POLYNOM1:29 ;
then A41: |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| <= Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| by Th15;
A42: dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) = dom (F1 /^ (k + 1)) by POLYNOM1:def 3;
A43: len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| = len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) by Def1
.= len (F1 /^ (k + 1)) by A42, FINSEQ_3:31
.= (len F1) - (k + 1) by A11, A19, RFINSEQ:def 2
.= len |.F2.| by A15, A19, Def1 ;

now

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 )
assume A44: 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 A45: i in Seg (len |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).|) by FINSEQ_1:def 3;
then i in Seg (len ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " ))) by Def1;
then A46: i in dom ((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) by FINSEQ_1:def 3;
A47: ((k + 1) + i) -' 1 = ((k + i) + 1) - 1 by XREAL_0:def 2
.= k + i ;
A48: len F2 = len |.F2.| by Def1;
then A49: dom F2 = dom |.F2.| by FINSEQ_3:31;
A50: i in dom F2 by A43, A45, A48, FINSEQ_1:def 3;
A51: (k + i) + 1 >= 0 + 1 by XREAL_1:8;
i <= len |.F2.| by A43, A45, FINSEQ_1:3;
then i <= (len F1) - (k + 1) by A15, A19, Def1;
then (k + 1) + i <= len F1 by XREAL_1:21;
then A52: (k + 1) + i in dom F1 by A51, FINSEQ_3:27;
i >= 0 + 1 by A45, FINSEQ_1:3;
then A53: i - 1 >= 0 by XREAL_1:21;
c to_power (i -' 1) <= 1 by A17, TBSP_1:2;
then A54: c to_power (i - 1) <= 1 by A53, XREAL_0:def 2;
A55: c to_power (k + i) > 0 by A17, POWER:39;
A56: |.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| >= 0 by COMPLEX1:132;
A57: ((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i)) = F2 . i by A16, A50
.= F2 /. i by A50, PARTFUN1:def 8 ;
A58: (F1 /^ (k + 1)) /. i = (F1 /^ (k + 1)) . i by A42, A46, PARTFUN1:def 8
.= F1 . ((k + 1) + i) by A11, A19, A42, A46, RFINSEQ:def 2
.= ((Subst p,<%z0,(1_ F_Complex )%>) . (((k + 1) + i) -' 1)) * ((power F_Complex ) . ([**c,0 **] * sq),(((k + 1) + i) -' 1)) by A20, A52
.= ((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * (((power F_Complex ) . sq,(k + i)) * ((power F_Complex ) . [**c,0 **],(k + i))) by A47, GROUP_1:100
.= (((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))) * ((power F_Complex ) . [**c,0 **],(k + i)) ;
A59: (k + i) - (k + 1) = i - 1 ;
|.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i = |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| /. i by A44, PARTFUN1:def 8
.= |.(((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )) /. i).| by A46, Def1
.= |.(((F1 /^ (k + 1)) /. i) * ([**(c to_power (k + 1)),0 **] " )).| by A42, A46, POLYNOM1:def 3
.= |.((F1 /^ (k + 1)) /. i).| * |.([**(c to_power (k + 1)),0 **] " ).| by COMPLFLD:109
.= |.((((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))) * ((power F_Complex ) . [**c,0 **],(k + i))).| * ((abs (c to_power (k + 1))) " ) by A34, A58, COMPLFLD:9, COMPLFLD:110
.= (|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * |.((power F_Complex ) . [**c,0 **],(k + i)).|) * ((abs (c to_power (k + 1))) " ) by COMPLFLD:109
.= (|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * |.[**(c to_power (k + i)),0 **].|) * ((abs (c to_power (k + 1))) " ) by A17, HAHNBAN1:37
.= (|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * (c to_power (k + i))) * ((abs (c to_power (k + 1))) " ) by A55, ABSVALUE:def 1
.= (|.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * (c to_power (k + i))) * ((c to_power (k + 1)) " ) by A34, ABSVALUE:def 1
.= |.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * ((c to_power (k + i)) * ((c to_power (k + 1)) " ))
.= |.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * ((c to_power (k + i)) / (c to_power (k + 1)))
.= |.(((Subst p,<%z0,(1_ F_Complex )%>) . (k + i)) * ((power F_Complex ) . sq,(k + i))).| * (c to_power (i - 1)) by A17, A59, POWER:34 ;
then |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.(F2 /. i).| by A54, A56, A57, XREAL_1:155;
then |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.F2.| /. i by A50, Def1;
hence |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| . i <= |.F2.| . i by A49, A50, PARTFUN1:def 8; :: thesis: verum

end;

then Sum |.((F1 /^ (k + 1)) * ([**(c to_power (k + 1)),0 **] " )).| <= Sum |.F2.| by A43, INTEGRA5:3;
then |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| <= Sum |.F2.| by A41, XXREAL_0:2;
then c * |.((Sum (F1 /^ (k + 1))) / [**(c to_power (k + 1)),0 **]).| <= c * (Sum |.F2.|) by A17, XREAL_1:66;
hence c * (Sum |.F2.|) >= |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| by A40, XXREAL_0:2; :: thesis: verum

end;

then |.((Subst p,<%z0,(1_ F_Complex )%>) . 0 ).| <= 0 by Lm1;
then A60: (Subst p,<%z0,(1_ F_Complex )%>) . 0 = 0. F_Complex by COMPLFLD:96;
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 A4, A60, Th32;
hence z0 is_a_root_of p by Def6; :: thesis: verum

end;

hence p is with_roots by Def7; :: thesis: verum

end;

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

set np = NormPolynomial p;
A62: len (NormPolynomial p) = len p by A61, Th58;
A63: len <%((NormPolynomial p) . 0 ),(1_ F_Complex )%> = 2 by Th41;
A64: (len p) -' 1 = 2 - 1 by A61, XREAL_0:def 2;

now

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

per cases ( k = 0 or k = 1 ) by A61, A62, A65, 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 Th39; :: thesis: verum

end;

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

hence (NormPolynomial p) . k = 1_ F_Complex by A61, A64, Th57
.= <%((NormPolynomial p) . 0 ),(1_ F_Complex )%> . k by A66, Th39 ;
:: thesis: verum

end;

end;

end;

then A67: NormPolynomial p = <%((NormPolynomial p) . 0 ),(1_ F_Complex )%> by A61, A62, A63, ALGSEQ_1:28;
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 A67, Th48
.= 0. F_Complex by RLVECT_1:16 ;
hence z0 is_a_root_of NormPolynomial p by Def6; :: thesis: verum

end;

then NormPolynomial p is with_roots by Def7;
hence p is with_roots by A61, Th61; :: thesis: verum

end;

end;