1 - 1 = 0 ;
then A1: 1 -' 1 = 0 by XREAL_1:233;
reconsider z2 = 1_ F_Complex as Element of COMPLEX by COMPLFLD:def 1;
let n be non zero 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:8;
then A6: 1 < len F by A3, Th40;
A7: len F = n + 1 by A3, Th40;
then (len F) - 1 = n ;
then A8: (len F) -' 1 = n by A5, XREAL_1:233;
((len F) - 1) + 1 = len F ;
then A9: ((len F) -' 1) + 1 = len F by A6, XREAL_1:233;
A10: (unital_poly (F_Complex,n)) . 0 = - (1_ F_Complex) by Th38;
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 CARD_1:def 7;
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:131;
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:131;
A13: 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:13;
hence (((len F) -' 1) |-> (0. F_Complex)) . i = 0. F_Complex by FUNCOP_1:7; :: thesis: verum

end;

A14: 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
A15: i <> 1 and
A16: i in dom R1 ; :: thesis: R1 . i = 0. F_Complex
A17: dom <*(- (1_ F_Complex))*> = Seg 1 by FINSEQ_1:def 8;

now :: thesis: not i in dom <*(- (1_ F_Complex))*>

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

end;

then consider j being Nat such that
A18: j in dom (((len F) -' 1) |-> (0. F_Complex)) and
A19: i = (len <*(- (1_ F_Complex))*>) + j by A16, FINSEQ_1:25;
(((len F) -' 1) |-> (0. F_Complex)) . j = 0. F_Complex by A13, A18;
hence R1 . i = 0. F_Complex by A18, A19, 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:22;
then A20: len ((((len F) -' 1) |-> (0. F_Complex)) ^ <*((power F_Complex) . (x,n))*>) = len F by A11, A9, FINSEQ_1:39;
A21: 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
A22: i in dom R2 and
A23: i <> len F ; :: thesis: R2 . i = 0. F_Complex
A24: dom R2 = Seg (len F) by A20, FINSEQ_1:def 3;
then i <= len F by A22, FINSEQ_1:1;
then i < ((len F) -' 1) + 1 by A9, A23, XXREAL_0:1;
then A25: i <= (len F) -' 1 by NAT_1:13;
1 <= i by A22, A24, FINSEQ_1:1;
then i in Seg ((len F) -' 1) by A25, FINSEQ_1:1;
then A26: 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 A13, A26; :: thesis: verum

end;

len R1 = len F by CARD_1:def 7;
then A27: dom R1 = Seg (len F) by FINSEQ_1:def 3;
len R2 = len F by CARD_1:def 7;
then A28: dom R2 = Seg (len F) by FINSEQ_1:def 3;
A29: R1 . 1 = - (1_ F_Complex) by FINSEQ_1:41;
A30: len (R1 + R2) = len F by CARD_1:def 7;
then A31: dom (R1 + R2) = Seg (len F) by FINSEQ_1:def 3;
A32: R2 . (len F) = (power F_Complex) . (x,n) by A11, A9, FINSEQ_1:42;
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 A33: k in dom (R1 + R2) ; :: thesis: (R1 + R2) . k = F . k
A34: k in Seg (len F) by A30, A33, FINSEQ_1:def 3;
A35: k in dom F by A31, A33, FINSEQ_1:def 3;
A36: 1 <= k by A31, A33, FINSEQ_1:1;
A37: (- (1_ F_Complex)) * (1_ F_Complex) = - (1_ F_Complex) ;

now :: thesis: (R1 + R2) . k = F . k

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

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

then R2 . k = 0. F_Complex by A6, A21, A28, A34;
then A39: (R1 + R2) . 1 = (- (1_ F_Complex)) + (0. F_Complex) by A29, A33, A38, FVSUM_1:17;
F . 1 = ((unital_poly (F_Complex,n)) . 0) * ((power F_Complex) . (x,0)) by A4, A1, A35, A38
.= - (1_ F_Complex) by A10, A37, GROUP_1:def 7 ;
hence (R1 + R2) . k = F . k by A38, A39, COMPLFLD:7; :: thesis: verum

end;

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

now :: thesis: (R1 + R2) . k = F . k

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

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

len F <> 0 by A3, A5, Th40;
then A42: F . (len F) = ((unital_poly (F_Complex,n)) . ((len F) -' 1)) * ((power F_Complex) . (x,((len F) -' 1))) by A4, A12, FINSEQ_1:3
.= (1_ F_Complex) * ((power F_Complex) . (x,n)) by A8, Th38
.= (power F_Complex) . (x,n) ;
R1 . (len F) = 0. F_Complex by A6, A14, A27, A34, A41;
then (R1 + R2) . (len F) = (0. F_Complex) + ((power F_Complex) . (x,n)) by A32, A33, A41, FVSUM_1:17
.= (power F_Complex) . (x,n) by COMPLFLD:7 ;
hence (R1 + R2) . k = F . k by A41, A42; :: thesis: verum

end;

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

A44: now :: thesis: not k -' 1 = n

assume k -' 1 = n ; :: thesis: contradiction
then k - 1 = n by A36, XREAL_1:233;
hence contradiction by A7, A43; :: thesis: verum

end;

1 < k by A36, A40, XXREAL_0:1;
then 1 + (- 1) < k + (- 1) by XREAL_1:8;
then 1 - 1 < k - 1 ;
then 0 < k -' 1 by A36, XREAL_1:233;
then (unital_poly (F_Complex,n)) . (k -' 1) = 0. F_Complex by A44, Th39;
then A45: F . k = (0. F_Complex) * ((power F_Complex) . (x,(k -' 1))) by A4, A35;
A46: R2 . k = 0. F_Complex by A21, A28, A34, A43;
R1 . k = 0. F_Complex by A14, A27, A34, A40;
then (R1 + R2) . k = (0. F_Complex) + (0. F_Complex) by A33, A46, FVSUM_1:17;
hence (R1 + R2) . k = F . k by A45, COMPLFLD:7; :: 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 A47: R1 + R2 = F by A12, A31, FINSEQ_1:13;
Sum (((len F) -' 1) |-> (0. F_Complex)) = 0. F_Complex by MATRIX_3:11;
then ( Sum R1 = (- (1_ F_Complex)) + (0. F_Complex) & Sum R2 = (0. F_Complex) + ((power F_Complex) . (x,n)) ) by FVSUM_1:71, FVSUM_1:72;
then ( - z2 = - (1_ F_Complex) & Sum F = (- (1_ F_Complex)) + ((power F_Complex) . (x,n)) ) by A47, COMPLFLD:2, COMPLFLD:7, FVSUM_1:76;
hence eval ((unital_poly (F_Complex,n)),x) = ((power F_Complex) . (x,n)) - 1 by A2, COMPLFLD:8; :: thesis: verum