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 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 ;
A10: dom d c= dom c by ;
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 )
A11: n > n - 1 by XREAL_1:146;
assume A12: i in dom e ; :: thesis: e . i = 0. L
then A13: 1 + i in dom c by ;
i <= n by ;
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 ;
then A15: n - i <= n - 1 by XREAL_1:13;
thus e . i = c . (1 + i) by
.= r . (x + (1 + i)) by
.= (p . ((x + (1 + i)) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + (1 + i)))) by
.= (p . ((x + (1 + i)) -' 1)) * (0. L) by
.= 0. L ; :: thesis: verum
end;
then A16: Sum e = 0. L by POLYNOM3:1;
now :: thesis: for i being Element of NAT st i in dom b holds
b . i = 0. L
let i be Element of NAT ; :: thesis: ( i in dom b implies b . i = 0. L )
A17: dom b c= dom r by ;
assume A18: i in dom b ; :: thesis: b . i = 0. L
then i <= x by ;
then i + n <= x + n by XREAL_1:6;
then i + n < (x + n) + 1 by NAT_1:13;
then A19: n < ((x + n) + 1) - i by XREAL_1:20;
then A20: ((x + n) + 1) - i = ((x + n) + 1) -' i by XREAL_0:def 2;
thus b . i = r . i by
.= (p . (i -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' i)) by A3, A18, A17
.= (p . (i -' 1)) * (0. L) by
.= 0. L ; :: thesis: verum
end;
then A21: Sum b = 0. L by POLYNOM3:1;
A22: 1 in dom d by ;
then d . 1 = c . 1 by
.= r . (x + 1) by
.= (p . ((x + 1) -' 1)) * ((monomial (a,n)) . (((x + n) + 1) -' (x + 1))) by
.= (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 ;
then Sum d = (p . x) * a by RLVECT_1:44;
then Sum c = ((p . x) * a) + (0. L) by
.= (p . x) * a by RLVECT_1:4 ;
hence (p *' (monomial (a,n))) . (x + n) = (0. L) + ((p . x) * a) by
.= (p . x) * a by RLVECT_1:4 ;
:: thesis: verum