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 (p *' (monomial a,n)) . (x + n) = (p . x) * a
let n, x be Element of NAT ; :: thesis: 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; :: thesis: for p being Polynomial of L holds (p *' (monomial a,n)) . (x + n) = (p . x) * a
let p be Polynomial of L; :: thesis: (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 11;
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:26;
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:26;
A10: dom d c= dom c by A9, FINSEQ_1:39;

now

let i be Element of NAT ; :: thesis: ( i in dom e implies e . i = 0. L )
A11: n > n - 1 by XREAL_1:148;
assume A12: i in dom e ; :: thesis: e . i = 0. L
then A13: 1 + i in dom c by A7, A9, FINSEQ_1:41;
i <= n by A8, A12, FINSEQ_3:27;
then x + i <= x + n by XREAL_1:8;
then (x + i) + 1 <= (x + n) + 1 by XREAL_1:8;
then A14: ((x + n) + 1) -' (x + (1 + i)) = ((x + n) + 1) - (x + (1 + i)) by XREAL_1:235;
1 <= i by A12, FINSEQ_3:27;
then A15: n - i <= n - 1 by XREAL_1:15;
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:41
.= (p . ((x + (1 + i)) -' 1)) * (0. L) by A14, A15, A11, Def5
.= 0. L by VECTSP_1:36 ; :: thesis: verum

end;

then A16: Sum e = 0. L by POLYNOM3:1;

now

let i be Element of NAT ; :: thesis: ( i in dom b implies b . i = 0. L )
A17: dom b c= dom r by A6, FINSEQ_1:39;
assume A18: i in dom b ; :: thesis: b . i = 0. L
then i <= x by A4, FINSEQ_3:27;
then i + n <= x + n by XREAL_1:8;
then i + n < (x + n) + 1 by NAT_1:13;
then A19: n < ((x + n) + 1) - i by XREAL_1:22;
then A20: ((x + n) + 1) - i = ((x + n) + 1) -' i by XREAL_0:def 2;
thus b . i = r . i by A6, A18, FINSEQ_1:def 7
.= (p . (i -' 1)) * ((monomial a,n) . (((x + n) + 1) -' i)) by A3, A18, A17
.= (p . (i -' 1)) * (0. L) by A19, A20, Def5
.= 0. L by VECTSP_1:36 ; :: thesis: verum

end;

then A21: Sum b = 0. L by POLYNOM3:1;
A22: 1 in dom d by A7, FINSEQ_3:27;
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:41
.= (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:57;
then Sum d = (p . x) * a by RLVECT_1:61;
then Sum c = ((p . x) * a) + (0. L) by A9, A16, RLVECT_1:58
.= (p . x) * a by RLVECT_1:10 ;
hence (p *' (monomial a,n)) . (x + n) = (0. L) + ((p . x) * a) by A2, A6, A21, RLVECT_1:58
.= (p . x) * a by RLVECT_1:10 ;
:: thesis: verum