1 - 1 = 0 ;
then A1: 1 -' 1 = 0 by XREAL_1:235;
reconsider z2 = 1_ F_Complex as Element of COMPLEX by COMPLFLD:def 1;
let n be non empty Element of NAT ; :: thesis: for x being Element of F_Complex holds eval (unital_poly F_Complex ,n),x = ((power F_Complex ) . x,n) - 1
let x be Element of F_Complex ; :: thesis: eval (unital_poly F_Complex ,n),x = ((power F_Complex ) . x,n) - 1
set p = unital_poly F_Complex ,n;
consider F being FinSequence of F_Complex such that
A2: eval (unital_poly F_Complex ,n),x = Sum F and
A3: len F = len (unital_poly F_Complex ,n) and
A4: for i being Element of NAT st i in dom F holds
F . i = ((unital_poly F_Complex ,n) . (i -' 1)) * ((power F_Complex ) . x,(i -' 1)) by POLYNOM4:def 2;
A5: 0 + 1 < n + 1 by XREAL_1:10;
then A6: 1 < len F by A3, Th44;
A7: len F = n + 1 by A3, Th44;
then (len F) - 1 = n ;
then A8: (len F) -' 1 = n by A5, XREAL_1:235;
((len F) - 1) + 1 = len F ;
then A9: ((len F) -' 1) + 1 = len F by A6, XREAL_1:235;
A10: (unital_poly F_Complex ,n) . 0 = - (1_ F_Complex ) by Th42;
set xn = (power F_Complex ) . x,n;
set null = ((len F) -' 1) |-> (0. F_Complex );
A11: len (((len F) -' 1) |-> (0. F_Complex )) = (len F) -' 1 by FINSEQ_1:def 18;
set tR2 = (((len F) -' 1) |-> (0. F_Complex )) ^ <*((power F_Complex ) . x,n)*>;
set tR1 = <*(- (1_ F_Complex ))*> ^ (((len F) -' 1) |-> (0. F_Complex ));
A12: dom F = Seg (len F) by FINSEQ_1:def 3;
Y: <*((power F_Complex ) . x,n)*> in 1 -tuples_on the carrier of F_Complex by FINSEQ_2:118;
X: <*(- (1_ F_Complex ))*> in 1 -tuples_on the carrier of F_Complex by FINSEQ_2:118;
A13: ((len F) -' 1) |-> (0. F_Complex ) is Element of ((len F) -' 1) -tuples_on the carrier of F_Complex by FINSEQ_2:132;
reconsider R1 = <*(- (1_ F_Complex ))*> ^ (((len F) -' 1) |-> (0. F_Complex )) as Tuple of len F,the carrier of F_Complex by A9, FINSEQ_2:127;
reconsider R1 = R1 as Element of (len F) -tuples_on the carrier of F_Complex by FINSEQ_2:151;
reconsider R2 = (((len F) -' 1) |-> (0. F_Complex )) ^ <*((power F_Complex ) . x,n)*> as Tuple of len F,the carrier of F_Complex by A9, FINSEQ_2:127;
reconsider R2 = R2 as Element of (len F) -tuples_on the carrier of F_Complex by FINSEQ_2:151;
A14: for i being Element of NAT st i in dom (((len F) -' 1) |-> (0. F_Complex )) holds
(((len F) -' 1) |-> (0. F_Complex )) . i = 0. F_Complex

proof

let i be Element of NAT ; :: thesis: ( i in dom (((len F) -' 1) |-> (0. F_Complex )) implies (((len F) -' 1) |-> (0. F_Complex )) . i = 0. F_Complex )
assume i in dom (((len F) -' 1) |-> (0. F_Complex )) ; :: thesis: (((len F) -' 1) |-> (0. F_Complex )) . i = 0. F_Complex
then i in Seg ((len F) -' 1) by FUNCOP_1:19;
hence (((len F) -' 1) |-> (0. F_Complex )) . i = 0. F_Complex by FUNCOP_1:13; :: thesis: verum

end;

A15: for i being Nat st i <> 1 & i in dom R1 holds
R1 . i = 0. F_Complex

proof

let i be Nat; :: thesis: ( i <> 1 & i in dom R1 implies R1 . i = 0. F_Complex )
assume that
A16: i <> 1 and
A17: i in dom R1 ; :: thesis: R1 . i = 0. F_Complex
A18: dom <*(- (1_ F_Complex ))*> = Seg 1 by FINSEQ_1:def 8;

now

assume i in dom <*(- (1_ F_Complex ))*> ; :: thesis: contradiction
then ( 1 <= i & i <= 1 ) by A18, FINSEQ_1:3;
hence contradiction by A16, XXREAL_0:1; :: thesis: verum

end;

then consider j being Nat such that
A19: j in dom (((len F) -' 1) |-> (0. F_Complex )) and
A20: i = (len <*(- (1_ F_Complex ))*>) + j by A17, FINSEQ_1:38;
(((len F) -' 1) |-> (0. F_Complex )) . j = 0. F_Complex by A14, A19;
hence R1 . i = 0. F_Complex by A19, A20, FINSEQ_1:def 7; :: thesis: verum

end;

len ((((len F) -' 1) |-> (0. F_Complex )) ^ <*((power F_Complex ) . x,n)*>) = (len (((len F) -' 1) |-> (0. F_Complex ))) + (len <*((power F_Complex ) . x,n)*>) by FINSEQ_1:35;
then A21: len ((((len F) -' 1) |-> (0. F_Complex )) ^ <*((power F_Complex ) . x,n)*>) = len F by A11, A9, FINSEQ_1:56;
A22: for i being Element of NAT st i in dom R2 & i <> len F holds
R2 . i = 0. F_Complex

proof

let i be Element of NAT ; :: thesis: ( i in dom R2 & i <> len F implies R2 . i = 0. F_Complex )
assume that
A23: i in dom R2 and
A24: i <> len F ; :: thesis: R2 . i = 0. F_Complex
A25: dom R2 = Seg (len F) by A21, FINSEQ_1:def 3;
then i <= len F by A23, FINSEQ_1:3;
then i < ((len F) -' 1) + 1 by A9, A24, XXREAL_0:1;
then A26: i <= (len F) -' 1 by NAT_1:13;
1 <= i by A23, A25, FINSEQ_1:3;
then i in Seg ((len F) -' 1) by A26, FINSEQ_1:3;
then A27: i in dom (((len F) -' 1) |-> (0. F_Complex )) by A11, FINSEQ_1:def 3;
then R2 . i = (((len F) -' 1) |-> (0. F_Complex )) . i by FINSEQ_1:def 7;
hence R2 . i = 0. F_Complex by A14, A27; :: thesis: verum

end;

len R1 = len F by FINSEQ_1:def 18;
then A28: dom R1 = Seg (len F) by FINSEQ_1:def 3;
len R2 = len F by FINSEQ_1:def 18;
then A29: dom R2 = Seg (len F) by FINSEQ_1:def 3;
A30: R1 . 1 = - (1_ F_Complex ) by FINSEQ_1:58;
A31: len (R1 + R2) = len F by FINSEQ_1:def 18;
then A32: dom (R1 + R2) = Seg (len F) by FINSEQ_1:def 3;
A33: R2 . (len F) = (power F_Complex ) . x,n by A11, A9, FINSEQ_1:59;
for k being Nat st k in dom (R1 + R2) holds
(R1 + R2) . k = F . k

proof

let k be Nat; :: thesis: ( k in dom (R1 + R2) implies (R1 + R2) . k = F . k )
assume A34: k in dom (R1 + R2) ; :: thesis: (R1 + R2) . k = F . k
A35: k in Seg (len F) by A31, A34, FINSEQ_1:def 3;
A36: k in dom F by A32, A34, FINSEQ_1:def 3;
A37: 1 <= k by A32, A34, FINSEQ_1:3;
A38: (- (1_ F_Complex )) * (1_ F_Complex ) = - (1_ F_Complex ) by COMPLFLD:10;

now

per cases ( k = 1 or k <> 1 ) ;

suppose A39: k = 1 ; :: thesis: (R1 + R2) . k = F . k

then R2 . k = 0. F_Complex by A6, A22, A29, A35;
then A40: (R1 + R2) . 1 = (- (1_ F_Complex )) + (0. F_Complex ) by A30, A34, A39, FVSUM_1:21;
F . 1 = ((unital_poly F_Complex ,n) . 0 ) * ((power F_Complex ) . x,0 ) by A4, A1, A36, A39
.= - (1_ F_Complex ) by A10, A38, GROUP_1:def 8 ;
hence (R1 + R2) . k = F . k by A39, A40, COMPLFLD:9; :: thesis: verum

end;

suppose A41: k <> 1 ; :: thesis: (R1 + R2) . k = F . k

now

per cases ( k = len F or k <> len F ) ;

suppose A42: k = len F ; :: thesis: (R1 + R2) . k = F . k

len F <> 0 by A3, A5, Th44;
then A43: F . (len F) = ((unital_poly F_Complex ,n) . ((len F) -' 1)) * ((power F_Complex ) . x,((len F) -' 1)) by A4, A12, FINSEQ_1:5
.= (1_ F_Complex ) * ((power F_Complex ) . x,n) by A8, Th42
.= (power F_Complex ) . x,n by VECTSP_1:def 19 ;
R1 . (len F) = 0. F_Complex by A6, A15, A28, A35, A42;
then (R1 + R2) . (len F) = (0. F_Complex ) + ((power F_Complex ) . x,n) by A33, A34, A42, FVSUM_1:21
.= (power F_Complex ) . x,n by COMPLFLD:9 ;
hence (R1 + R2) . k = F . k by A42, A43; :: thesis: verum

end;

suppose A44: k <> len F ; :: thesis: (R1 + R2) . k = F . k

A45: now

assume k -' 1 = n ; :: thesis: contradiction
then k - 1 = n by A37, XREAL_1:235;
hence contradiction by A7, A44; :: thesis: verum

end;

1 < k by A37, A41, XXREAL_0:1;
then 1 + (- 1) < k + (- 1) by XREAL_1:10;
then 1 - 1 < k - 1 ;
then 0 < k -' 1 by A37, XREAL_1:235;
then (unital_poly F_Complex ,n) . (k -' 1) = 0. F_Complex by A45, Th43;
then A46: F . k = (0. F_Complex ) * ((power F_Complex ) . x,(k -' 1)) by A4, A36;
A47: R2 . k = 0. F_Complex by A22, A29, A35, A44;
R1 . k = 0. F_Complex by A15, A28, A35, A41;
then (R1 + R2) . k = (0. F_Complex ) + (0. F_Complex ) by A34, A47, FVSUM_1:21;
hence (R1 + R2) . k = F . k by A46, COMPLFLD:9; :: thesis: verum

end;

end;

end;

hence (R1 + R2) . k = F . k ; :: thesis: verum

end;

end;

end;

hence (R1 + R2) . k = F . k ; :: thesis: verum

end;

then A48: R1 + R2 = F by A12, A32, FINSEQ_1:17;
Sum (((len F) -' 1) |-> (0. F_Complex )) = 0. F_Complex by MATRIX_3:13;
then ( Sum R1 = (- (1_ F_Complex )) + (0. F_Complex ) & Sum R2 = (0. F_Complex ) + ((power F_Complex ) . x,n) ) by FVSUM_1:87, FVSUM_1:89;
then ( - z2 = - (1_ F_Complex ) & Sum F = (- (1_ F_Complex )) + ((power F_Complex ) . x,n) ) by A48, COMPLFLD:4, COMPLFLD:9, FVSUM_1:95;
hence eval (unital_poly F_Complex ,n),x = ((power F_Complex ) . x,n) - 1 by A2, COMPLFLD:10; :: thesis: verum