let L be non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for x, z being Element of L holds eval (rpoly 1,z),x = x - z
let x, z be Element of L; :: thesis: eval (rpoly 1,z),x = x - z
set p = rpoly 1,z;
consider F being FinSequence of L 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 L) . x,(n -' 1)) ) ) by POLYNOM4:def 2;
A2: deg (rpoly 1,z) = 1 by Th27;
then A3: F = <*(F . 1),(F . 2)*> by A1, FINSEQ_1:61
.= <*(F . 1)*> ^ <*(F . 2)*> ;
A4: 1 -' 1 = 1 - 1 by XREAL_0:def 2;
1 in Seg (len F) by A1, A2, FINSEQ_1:4;
then 1 in dom F by FINSEQ_1:def 3;
then A5: F . 1 = ((rpoly 1,z) . 0 ) * ((power L) . x,(1 -' 1)) by A1, A4
.= ((rpoly 1,z) . 0 ) * (1_ L) by A4, GROUP_1:def 8
.= (rpoly 1,z) . 0 by VECTSP_1:def 13
.= - ((power L) . z,(1 + 0 )) by Lm11
.= - (((power L) . z,0 ) * z) by GROUP_1:def 8
.= - ((1_ L) * z) by GROUP_1:def 8
.= - z by VECTSP_1:def 19 ;
A6: 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 L) . x,(1 + 0 )) by A1, A6
.= ((rpoly 1,z) . 1) * (((power L) . x,0 ) * x) by GROUP_1:def 8
.= ((rpoly 1,z) . 1) * ((1_ L) * x) by GROUP_1:def 8
.= ((rpoly 1,z) . 1) * x by VECTSP_1:def 19
.= (1_ L) * x by Lm11
.= x by VECTSP_1:def 19 ;
hence eval (rpoly 1,z),x = (Sum <*(- z)*>) + (Sum <*x*>) by A1, A3, A5, 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