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;

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

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

then A15:
Sum b = 0. L
by POLYNOM3:1;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;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

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

e . i = 0. L

then A20:
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 )

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;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

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