let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
let n, x be Element of NAT ; for a being Element of L
for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
let a be Element of L; for p being Polynomial of L holds (p *' (monomial (a,n))) . (x + n) = (p . x) * a
let p be Polynomial of L; (p *' (monomial (a,n))) . (x + n) = (p . x) * a
consider r being FinSequence of the carrier of L such that
A1:
len r = (x + n) + 1
and
A2:
(p *' (monomial (a,n))) . (x + n) = Sum r
and
A3:
for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' k))
by POLYNOM3:def 9;
len r = x + (n + 1)
by A1;
then consider b, c being FinSequence of the carrier of L such that
A4:
len b = x
and
A5:
len c = n + 1
and
A6:
r = b ^ c
by FINSEQ_2:23;
consider d, e being FinSequence of the carrier of L such that
A7:
len d = 1
and
A8:
len e = n
and
A9:
c = d ^ e
by A5, FINSEQ_2:23;
A10:
dom d c= dom c
by A9, FINSEQ_1:26;
now for i being Element of NAT st i in dom e holds
e . i = 0. Llet i be
Element of
NAT ;
( i in dom e implies e . i = 0. L )A11:
n > n - 1
by XREAL_1:146;
assume A12:
i in dom e
;
e . i = 0. Lthen A13:
1
+ i in dom c
by A7, A9, FINSEQ_1:28;
i <= n
by A8, A12, FINSEQ_3:25;
then
x + i <= x + n
by XREAL_1:6;
then
(x + i) + 1
<= (x + n) + 1
by XREAL_1:6;
then A14:
((x + n) + 1) -' (x + (1 + i)) = ((x + n) + 1) - (x + (1 + i))
by XREAL_1:233;
1
<= i
by A12, FINSEQ_3:25;
then A15:
n - i <= n - 1
by XREAL_1:13;
thus e . i =
c . (1 + i)
by A7, A9, A12, FINSEQ_1:def 7
.=
r . (x + (1 + i))
by A4, A6, A13, FINSEQ_1:def 7
.=
(p . ((x + (1 + i)) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + (1 + i))))
by A3, A4, A6, A13, FINSEQ_1:28
.=
(p . ((x + (1 + i)) -' 1)) * (0. L)
by A14, A15, A11, Def5
.=
0. L
;
verum end;
then A16:
Sum e = 0. L
by POLYNOM3:1;
then A21:
Sum b = 0. L
by POLYNOM3:1;
A22:
1 in dom d
by A7, FINSEQ_3:25;
then d . 1 =
c . 1
by A9, FINSEQ_1:def 7
.=
r . (x + 1)
by A4, A6, A22, A10, FINSEQ_1:def 7
.=
(p . ((x + 1) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + 1)))
by A3, A4, A6, A22, A10, FINSEQ_1:28
.=
(p . x) * ((monomial (a,n)) . ((n + (x + 1)) -' (x + 1)))
by NAT_D:34
.=
(p . x) * ((monomial (a,n)) . n)
by NAT_D:34
.=
(p . x) * a
by Def5
;
then
d = <*((p . x) * a)*>
by A7, FINSEQ_1:40;
then
Sum d = (p . x) * a
by RLVECT_1:44;
then Sum c =
((p . x) * a) + (0. L)
by A9, A16, RLVECT_1:41
.=
(p . x) * a
by RLVECT_1:4
;
hence (p *' (monomial (a,n))) . (x + n) =
(0. L) + ((p . x) * a)
by A2, A6, A21, RLVECT_1:41
.=
(p . x) * a
by RLVECT_1:4
;
verum