let x, z be Element of F_Complex ; :: thesis: 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 & len F = len ((rpoly 1,z) *' ) & ( 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;
A2: deg ((rpoly 1,z) *' ) = deg (rpoly 1,z) by Th42
.= 1 by Th27 ;
then A3: len ((rpoly 1,z) *' ) = 1 + 1 ;
A4: F = <*(F . 1),(F . 2)*> by A1, A2, FINSEQ_1:61
.= <*(F . 1)*> ^ <*(F . 2)*> ;
A5: 1 -' 1 = 1 - 1 by XREAL_0:def 2;
A6: (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 in Seg (len F) by A1, A3;
then 1 in dom F by FINSEQ_1:def 3;
then A7: F . 1 = (((rpoly 1,z) *' ) . 0 ) * ((power F_Complex ) . x,0 ) by A1, A5
.= (((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 A6, Def9
.= (1_ F_Complex ) * ((- z) *' ) by GROUP_1:def 8
.= (- z) *' by VECTSP_1:def 19
.= - (z *' ) by COMPLFLD:88 ;
A8: 2 -' 1 = 2 - 1 by XREAL_0:def 2;
2 in Seg (len F) by A1, A2;
then 2 in dom F by FINSEQ_1:def 3;
then F . 2 = (((rpoly 1,z) *' ) . 1) * ((power F_Complex ) . x,(1 + 0 )) by A1, A8
.= (((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 ;
hence eval ((rpoly 1,z) *' ),x = (Sum <*(- (z *' ))*>) + (Sum <*(- x)*>) by A1, A4, A7, RLVECT_1:58
.= (Sum <*(- (z *' ))*>) + (- x) by RLVECT_1:61
.= (- (z *' )) + (- x) by RLVECT_1:61
.= (- x) - (z *' ) by RLVECT_1:def 12 ;
:: thesis: verum