let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for n, x being Element of NAT
for a being Element of L
for p being Polynomial of L holds ((monomial a,n) *' p) . (x + n) = a * (p . x)
let n, x be Element of NAT ; :: thesis: for a being Element of L
for p being Polynomial of L holds ((monomial a,n) *' p) . (x + n) = a * (p . x)
let a be Element of L; :: thesis: for p being Polynomial of L holds ((monomial a,n) *' p) . (x + n) = a * (p . x)
let p be Polynomial of L; :: thesis: ((monomial a,n) *' p) . (x + n) = a * (p . x)
consider r being FinSequence of the carrier of L such that
A1:
( len r = (x + n) + 1 & ((monomial a,n) *' p) . (x + n) = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = ((monomial a,n) . (k -' 1)) * (p . (((x + n) + 1) -' k)) ) )
by POLYNOM3:def 11;
len r = n + (1 + x)
by A1;
then consider b, c being FinSequence of the carrier of L such that
A2:
( len b = n & len c = 1 + x & r = b ^ c )
by FINSEQ_2:26;
consider d, e being FinSequence of the carrier of L such that
A3:
( len d = 1 & len e = x & c = d ^ e )
by A2, FINSEQ_2:26;
now let i be
Element of
NAT ;
:: thesis: ( i in dom b implies b . i = 0. L )assume A4:
i in dom b
;
:: thesis: b . i = 0. Lthen A5:
( 1
<= i &
i <= n )
by A2, FINSEQ_3:27;
then A6:
i -' 1
= i - 1
by XREAL_1:235;
A7:
i - 1
< i
by XREAL_1:148;
A8:
dom b c= dom r
by A2, FINSEQ_1:39;
thus b . i =
r . i
by A2, A4, FINSEQ_1:def 7
.=
((monomial a,n) . (i -' 1)) * (p . (((x + n) + 1) -' i))
by A1, A4, A8
.=
(0. L) * (p . (((x + n) + 1) -' i))
by A5, A6, A7, Def5
.=
0. L
by VECTSP_1:39
;
:: thesis: verum end;
then A9:
Sum b = 0. L
by POLYNOM3:1;
A10:
1 in dom d
by A3, FINSEQ_3:27;
A11:
dom d c= dom c
by A3, FINSEQ_1:39;
d . 1 =
c . 1
by A3, A10, FINSEQ_1:def 7
.=
r . (n + 1)
by A2, A10, A11, FINSEQ_1:def 7
.=
((monomial a,n) . ((n + 1) -' 1)) * (p . (((x + n) + 1) -' (n + 1)))
by A1, A2, A10, A11, FINSEQ_1:41
.=
((monomial a,n) . n) * (p . ((x + (n + 1)) -' (n + 1)))
by NAT_D:34
.=
((monomial a,n) . n) * (p . x)
by NAT_D:34
.=
a * (p . x)
by Def5
;
then
d = <*(a * (p . x))*>
by A3, FINSEQ_1:57;
then A12:
Sum d = a * (p . x)
by RLVECT_1:61;
now let i be
Element of
NAT ;
:: thesis: ( i in dom e implies e . i = 0. L )assume A13:
i in dom e
;
:: thesis: e . i = 0. Lthen A14:
1
+ i in dom c
by A3, FINSEQ_1:41;
i >= 1
by A13, FINSEQ_3:27;
then
n + i >= n + 1
by XREAL_1:8;
then A15:
n + i > n
by NAT_1:13;
A16:
(n + (1 + i)) -' 1 =
((n + i) + 1) -' 1
.=
n + i
by NAT_D:34
;
thus e . i =
c . (1 + i)
by A3, A13, FINSEQ_1:def 7
.=
r . (n + (1 + i))
by A2, A14, FINSEQ_1:def 7
.=
((monomial a,n) . ((n + (1 + i)) -' 1)) * (p . (((x + n) + 1) -' (n + (1 + i))))
by A1, A2, A14, FINSEQ_1:41
.=
(0. L) * (p . (((x + n) + 1) -' (n + (1 + i))))
by A15, A16, Def5
.=
0. L
by VECTSP_1:39
;
:: thesis: verum end;
then
Sum e = 0. L
by POLYNOM3:1;
then Sum c =
(a * (p . x)) + (0. L)
by A3, A12, RLVECT_1:58
.=
a * (p . x)
by RLVECT_1:10
;
hence ((monomial a,n) *' p) . (x + n) =
(0. L) + (a * (p . x))
by A1, A2, A9, RLVECT_1:58
.=
a * (p . x)
by RLVECT_1:10
;
:: thesis: verum