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

R1 . i = 0. F_Complex

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

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

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

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

A14:
for i being Nat st i <> 1 & i in dom R1 holds
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;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

R1 . i = 0. F_Complex

proof

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;
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;

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;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))*>

then consider j being Nat such that 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 ( 1 <= i & i <= 1 ) by A17, FINSEQ_1:1;

hence contradiction by A15, XXREAL_0:1; :: thesis: verum

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

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

len R1 = len F
by CARD_1:def 7;
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;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

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

then A47:
R1 + R2 = F
by A12, A31, FINSEQ_1:13;
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) ;

end;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 . kend;

hence
(R1 + R2) . k = F . k
; :: thesis: verumper cases
( k = 1 or k <> 1 )
;

end;

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;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

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

end;

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

hence
(R1 + R2) . k = F . k
; :: thesis: verumper cases
( k = len F or k <> len F )
;

end;

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;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

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

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;

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

1 < k
by A36, A40, XXREAL_0:1;assume
k -' 1 = n
; :: thesis: contradiction

then k - 1 = n by A36, XREAL_1:233;

hence contradiction by A7, A43; :: thesis: verum

end;then k - 1 = n by A36, XREAL_1:233;

hence contradiction by A7, A43; :: thesis: verum

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

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