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 and
A2: ((monomial (a,n)) *' p) . (x + n) = Sum r and
A3: 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 9;
len r = n + (1 + x) by A1;
then consider b, c being FinSequence of the carrier of L such that
A4: len b = n and
A5: len c = 1 + x 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
len e = x and
A8: c = d ^ e by A5, FINSEQ_2:23;
A9: dom d c= dom c by A8, FINSEQ_1:26;

now :: thesis: for i being Element of NAT st i in dom b holds
b . i = 0. L

A10: dom b c= dom r by A6, FINSEQ_1:26;
let i be Element of NAT ; :: thesis: ( i in dom b implies b . i = 0. L )
A11: i - 1 < i by XREAL_1:146;
assume A12: i in dom b ; :: thesis: b . i = 0. L
then A13: i <= n by A4, FINSEQ_3:25;
1 <= i by A12, FINSEQ_3:25;
then A14: i -' 1 = i - 1 by XREAL_1:233;
thus b . i = r . i by A6, A12, FINSEQ_1:def 7
.= ((monomial (a,n)) . (i -' 1)) * (p . (((x + n) + 1) -' i)) by A3, A12, A10
.= (0. L) * (p . (((x + n) + 1) -' i)) by A13, A14, A11, Def5
.= 0. L ; :: thesis: verum

end;

then A15: Sum b = 0. L by POLYNOM3:1;

now :: thesis: for i being Element of NAT st i in dom e holds
e . i = 0. L

let i be Element of NAT ; :: thesis: ( i in dom e implies e . i = 0. L )
A16: (n + (1 + i)) -' 1 = ((n + i) + 1) -' 1
.= n + i by NAT_D:34 ;
assume A17: i in dom e ; :: thesis: e . i = 0. L
then A18: 1 + i in dom c by A7, A8, FINSEQ_1:28;
i >= 1 by A17, FINSEQ_3:25;
then n + i >= n + 1 by XREAL_1:6;
then A19: n + i > n by NAT_1:13;
thus e . i = c . (1 + i) by A7, A8, A17, FINSEQ_1:def 7
.= r . (n + (1 + i)) by A4, A6, A18, FINSEQ_1:def 7
.= ((monomial (a,n)) . ((n + (1 + i)) -' 1)) * (p . (((x + n) + 1) -' (n + (1 + i)))) by A3, A4, A6, A18, FINSEQ_1:28
.= (0. L) * (p . (((x + n) + 1) -' (n + (1 + i)))) by A19, A16, Def5
.= 0. L ; :: thesis: verum

end;

then A20: Sum e = 0. L by POLYNOM3:1;
A21: 1 in dom d by A7, FINSEQ_3:25;
then d . 1 = c . 1 by A8, FINSEQ_1:def 7
.= r . (n + 1) by A4, A6, A21, A9, FINSEQ_1:def 7
.= ((monomial (a,n)) . ((n + 1) -' 1)) * (p . (((x + n) + 1) -' (n + 1))) by A3, A4, A6, A21, A9, FINSEQ_1:28
.= ((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 A7, FINSEQ_1:40;
then Sum d = a * (p . x) by RLVECT_1:44;
then Sum c = (a * (p . x)) + (0. L) by A8, A20, RLVECT_1:41
.= a * (p . x) by RLVECT_1:4 ;
hence ((monomial (a,n)) *' p) . (x + n) = (0. L) + (a * (p . x)) by A2, A6, A15, RLVECT_1:41
.= a * (p . x) by RLVECT_1:4 ;
:: thesis: verum