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;
reconsider R1 = <*(- (1_ F_Complex))*> ^ (((len F) -' 1) |-> (0. F_Complex)) as Tuple of len F, the carrier of F_Complex by A9;
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;
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