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:44
.=
<*(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 7
.=
((rpoly (1,z)) . 1) * ((1_ L) * x)
by GROUP_1:def 7
.=
((rpoly (1,z)) . 1) * x
.=
(1_ L) * x
by Lm10
.=
x
;
1 in Seg (len F)
by A4, A6, FINSEQ_1:2;
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 7
.=
(rpoly (1,z)) . 0
.=
- ((power L) . (z,(1 + 0)))
by Lm10
.=
- (((power L) . (z,0)) * z)
by GROUP_1:def 7
.=
- ((1_ L) * z)
by GROUP_1:def 7
.=
- z
;
hence eval ((rpoly (1,z)),x) =
(Sum <*(- z)*>) + (Sum <*x*>)
by A3, A7, 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