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:61
.=
<*(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 8
.=
(((rpoly 1,z) *' ) . 1) * ((1_ F_Complex ) * x)
by GROUP_1:def 8
.=
(((rpoly 1,z) *' ) . 1) * x
by VECTSP_1:def 19
.=
(((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 Lm11, COMPLFLD:85
.=
((power F_Complex ) . (- (1_ F_Complex )),(1 + 0 )) * x
by VECTSP_1:def 13
.=
(((power F_Complex ) . (- (1_ F_Complex )),0 ) * (- (1_ F_Complex ))) * x
by GROUP_1:def 8
.=
((1_ F_Complex ) * (- (1_ F_Complex ))) * x
by GROUP_1:def 8
.=
(- (1_ F_Complex )) * x
by VECTSP_1:def 13
.=
- ((1_ F_Complex ) * x)
by VECTSP_1:41
.=
- x
by VECTSP_1:def 19
;
A9: (rpoly 1,z) . 0 =
- ((power F_Complex ) . z,(1 + 0 ))
by Lm11
.=
- (((power F_Complex ) . z,0 ) * z)
by GROUP_1:def 8
.=
- ((1_ F_Complex ) * z)
by GROUP_1:def 8
.=
- z
by VECTSP_1:def 19
;
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 8
.=
((rpoly 1,z) *' ) . 0
by VECTSP_1:def 13
.=
((power F_Complex ) . (- (1_ F_Complex )),0 ) * ((- z) *' )
by A9, Def9
.=
(1_ F_Complex ) * ((- z) *' )
by GROUP_1:def 8
.=
(- z) *'
by VECTSP_1:def 19
.=
- (z *' )
by COMPLFLD:88
;
hence eval ((rpoly 1,z) *' ),x =
(Sum <*(- (z *' ))*>) + (Sum <*(- x)*>)
by A1, A5, A8, RLVECT_1:58
.=
(Sum <*(- (z *' ))*>) + (- x)
by RLVECT_1:61
.=
(- (z *' )) + (- x)
by RLVECT_1:61
.=
(- x) - (z *' )
by RLVECT_1:def 12
;
verum