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 A5, FINSEQ_2:23;

A10: dom d c= dom c by A9, FINSEQ_1:26;

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 ;

:: thesis: verum

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 A5, FINSEQ_2:23;

A10: dom d c= dom c by A9, FINSEQ_1:26;

now :: thesis: for i being Element of NAT st i in dom e holds

e . i = 0. L

then A16:
Sum e = 0. L
by POLYNOM3:1;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 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 ; :: thesis: verum

end;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 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 ; :: thesis: verum

now :: thesis: for i being Element of NAT st i in dom b holds

b . i = 0. L

then A21:
Sum b = 0. L
by POLYNOM3:1;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 A6, FINSEQ_1:26;

assume A18: i in dom b ; :: thesis: b . i = 0. L

then i <= x by A4, FINSEQ_3:25;

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 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 ; :: thesis: verum

end;A17: dom b c= dom r by A6, FINSEQ_1:26;

assume A18: i in dom b ; :: thesis: b . i = 0. L

then i <= x by A4, FINSEQ_3:25;

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 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 ; :: thesis: verum

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 ;

:: thesis: verum