let x, z be Element of F_Complex; eval (((rpoly (1,z)) *'),x) = (- x) - (z *')
set p = (rpoly (1,z)) *' ;
consider F being FinSequence of F_Complex such that
A1:
eval (((rpoly (1,z)) *'),x) = Sum F
and
A2:
len F = len ((rpoly (1,z)) *')
and
A3:
for n being Element of NAT st n in dom F holds
F . n = (((rpoly (1,z)) *') . (n -' 1)) * ((power F_Complex) . (x,(n -' 1)))
by POLYNOM4:def 2;
A4: deg ((rpoly (1,z)) *') =
deg (rpoly (1,z))
by Th42
.=
1
by Th27
;
then A5: F =
<*(F . 1),(F . 2)*>
by A2, FINSEQ_1:44
.=
<*(F . 1)*> ^ <*(F . 2)*>
;
len ((rpoly (1,z)) *') = 1 + 1
by A4;
then
1 in Seg (len F)
by A2;
then A6:
1 in dom F
by FINSEQ_1:def 3;
A7:
2 -' 1 = 2 - 1
by XREAL_0:def 2;
2 in Seg (len F)
by A2, A4;
then
2 in dom F
by FINSEQ_1:def 3;
then A8: F . 2 =
(((rpoly (1,z)) *') . 1) * ((power F_Complex) . (x,(1 + 0)))
by A3, A7
.=
(((rpoly (1,z)) *') . 1) * (((power F_Complex) . (x,0)) * x)
by GROUP_1:def 7
.=
(((rpoly (1,z)) *') . 1) * ((1_ F_Complex) * x)
by GROUP_1:def 7
.=
(((rpoly (1,z)) *') . 1) * x
.=
(((power F_Complex) . ((- (1_ F_Complex)),1)) * (((rpoly (1,z)) . 1) *')) * x
by Def9
.=
(((power F_Complex) . ((- (1_ F_Complex)),1)) * (1_ F_Complex)) * x
by Lm10, COMPLFLD:49
.=
((power F_Complex) . ((- (1_ F_Complex)),(1 + 0))) * x
.=
(((power F_Complex) . ((- (1_ F_Complex)),0)) * (- (1_ F_Complex))) * x
by GROUP_1:def 7
.=
((1_ F_Complex) * (- (1_ F_Complex))) * x
by GROUP_1:def 7
.=
(- (1_ F_Complex)) * x
.=
- ((1_ F_Complex) * x)
by VECTSP_1:9
.=
- x
;
A9: (rpoly (1,z)) . 0 =
- ((power F_Complex) . (z,(1 + 0)))
by Lm10
.=
- (((power F_Complex) . (z,0)) * z)
by GROUP_1:def 7
.=
- ((1_ F_Complex) * z)
by GROUP_1:def 7
.=
- z
;
1 -' 1 = 1 - 1
by XREAL_0:def 2;
then F . 1 =
(((rpoly (1,z)) *') . 0) * ((power F_Complex) . (x,0))
by A3, A6
.=
(((rpoly (1,z)) *') . 0) * (1_ F_Complex)
by GROUP_1:def 7
.=
((rpoly (1,z)) *') . 0
.=
((power F_Complex) . ((- (1_ F_Complex)),0)) * ((- z) *')
by A9, Def9
.=
(1_ F_Complex) * ((- z) *')
by GROUP_1:def 7
.=
(- z) *'
.=
- (z *')
by COMPLFLD:52
;
hence eval (((rpoly (1,z)) *'),x) =
(Sum <*(- (z *'))*>) + (Sum <*(- x)*>)
by A1, A5, A8, RLVECT_1:41
.=
(Sum <*(- (z *'))*>) + (- x)
by RLVECT_1:44
.=
(- (z *')) + (- x)
by RLVECT_1:44
.=
(- x) - (z *')
by RLVECT_1:def 11
;
verum