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