let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for a, b being Element of L

for p being Polynomial of L holds

( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )

let a, b be Element of L; :: thesis: for p being Polynomial of L holds

( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )

let q be Polynomial of L; :: thesis: ( (<%a,b%> *' q) . 0 = a * (q . 0) & ( for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) ) )

set p = <%a,b%>;

consider r being FinSequence of L such that

A1: len r = 0 + 1 and

A2: (<%a,b%> *' q) . 0 = Sum r and

A3: for k being Element of NAT st k in dom r holds

r . k = (<%a,b%> . (k -' 1)) * (q . ((0 + 1) -' k)) by POLYNOM3:def 9;

A4: 1 in dom r by A1, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of L by FINSEQ_2:11;

r = <*r1*> by A1, FINSEQ_1:40;

then Sum r = r1 by RLVECT_1:44

.= (<%a,b%> . (1 -' 1)) * (q . ((0 + 1) -' 1)) by A3, A4

.= (<%a,b%> . 0) * (q . ((0 + 1) -' 1)) by XREAL_1:232

.= (<%a,b%> . 0) * (q . 0) by NAT_D:34 ;

hence (<%a,b%> *' q) . 0 = a * (q . 0) by A2, POLYNOM5:38; :: thesis: for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))

let i be Nat; :: thesis: (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))

consider r being FinSequence of L such that

A5: len r = (i + 1) + 1 and

A6: (<%a,b%> *' q) . (i + 1) = Sum r and

A7: for k being Element of NAT st k in dom r holds

r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by POLYNOM3:def 9;

len r = i + 2 by A5;

then A8: 0 + 2 <= len r by XREAL_1:6;

then A9: 2 in dom r by FINSEQ_3:25;

then A10: r /. 2 = r . 2 by PARTFUN1:def 6

.= (<%a,b%> . ((1 + 1) -' 1)) * (q . (((i + 1) + 1) -' 2)) by A7, A9

.= (<%a,b%> . 1) * (q . (((i + 1) + 1) -' 2)) by NAT_D:34

.= b * (q . ((i + (1 + 1)) -' 2)) by POLYNOM5:38

.= b * (q . i) by NAT_D:34 ;

then A16: 1 in dom r by FINSEQ_3:25;

then r /. 1 = r . 1 by PARTFUN1:def 6

.= (<%a,b%> . (1 -' 1)) * (q . (((i + 1) + 1) -' 1)) by A7, A16

.= (<%a,b%> . 0) * (q . (((i + 1) + 1) -' 1)) by XREAL_1:232

.= (<%a,b%> . 0) * (q . (i + 1)) by NAT_D:34

.= a * (q . (i + 1)) by POLYNOM5:38 ;

hence (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) by A6, A8, A10, A11, Th2; :: thesis: verum

for p being Polynomial of L holds

( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )

let a, b be Element of L; :: thesis: for p being Polynomial of L holds

( (<%a,b%> *' p) . 0 = a * (p . 0) & ( for i being Nat holds (<%a,b%> *' p) . (i + 1) = (a * (p . (i + 1))) + (b * (p . i)) ) )

let q be Polynomial of L; :: thesis: ( (<%a,b%> *' q) . 0 = a * (q . 0) & ( for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) ) )

set p = <%a,b%>;

consider r being FinSequence of L such that

A1: len r = 0 + 1 and

A2: (<%a,b%> *' q) . 0 = Sum r and

A3: for k being Element of NAT st k in dom r holds

r . k = (<%a,b%> . (k -' 1)) * (q . ((0 + 1) -' k)) by POLYNOM3:def 9;

A4: 1 in dom r by A1, FINSEQ_3:25;

then reconsider r1 = r . 1 as Element of L by FINSEQ_2:11;

r = <*r1*> by A1, FINSEQ_1:40;

then Sum r = r1 by RLVECT_1:44

.= (<%a,b%> . (1 -' 1)) * (q . ((0 + 1) -' 1)) by A3, A4

.= (<%a,b%> . 0) * (q . ((0 + 1) -' 1)) by XREAL_1:232

.= (<%a,b%> . 0) * (q . 0) by NAT_D:34 ;

hence (<%a,b%> *' q) . 0 = a * (q . 0) by A2, POLYNOM5:38; :: thesis: for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))

let i be Nat; :: thesis: (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))

consider r being FinSequence of L such that

A5: len r = (i + 1) + 1 and

A6: (<%a,b%> *' q) . (i + 1) = Sum r and

A7: for k being Element of NAT st k in dom r holds

r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by POLYNOM3:def 9;

len r = i + 2 by A5;

then A8: 0 + 2 <= len r by XREAL_1:6;

then A9: 2 in dom r by FINSEQ_3:25;

then A10: r /. 2 = r . 2 by PARTFUN1:def 6

.= (<%a,b%> . ((1 + 1) -' 1)) * (q . (((i + 1) + 1) -' 2)) by A7, A9

.= (<%a,b%> . 1) * (q . (((i + 1) + 1) -' 2)) by NAT_D:34

.= b * (q . ((i + (1 + 1)) -' 2)) by POLYNOM5:38

.= b * (q . i) by NAT_D:34 ;

A11: now :: thesis: for k being Element of NAT st 2 < k & k in dom r holds

r . k = 0. L

1 <= len r
by A8, XXREAL_0:2;r . k = 0. L

let k be Element of NAT ; :: thesis: ( 2 < k & k in dom r implies r . k = 0. L )

assume that

A12: 2 < k and

A13: k in dom r ; :: thesis: r . k = 0. L

consider k1 being Nat such that

A14: k = k1 + 1 by A12, NAT_1:6;

A15: 2 <= k1 by A12, A14, NAT_1:13;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

thus r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by A7, A13

.= (<%a,b%> . k1) * (q . (((i + 1) + 1) -' k)) by A14, NAT_D:34

.= (0. L) * (q . (((i + 1) + 1) -' k)) by A15, POLYNOM5:38

.= 0. L ; :: thesis: verum

end;assume that

A12: 2 < k and

A13: k in dom r ; :: thesis: r . k = 0. L

consider k1 being Nat such that

A14: k = k1 + 1 by A12, NAT_1:6;

A15: 2 <= k1 by A12, A14, NAT_1:13;

reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;

thus r . k = (<%a,b%> . (k -' 1)) * (q . (((i + 1) + 1) -' k)) by A7, A13

.= (<%a,b%> . k1) * (q . (((i + 1) + 1) -' k)) by A14, NAT_D:34

.= (0. L) * (q . (((i + 1) + 1) -' k)) by A15, POLYNOM5:38

.= 0. L ; :: thesis: verum

then A16: 1 in dom r by FINSEQ_3:25;

then r /. 1 = r . 1 by PARTFUN1:def 6

.= (<%a,b%> . (1 -' 1)) * (q . (((i + 1) + 1) -' 1)) by A7, A16

.= (<%a,b%> . 0) * (q . (((i + 1) + 1) -' 1)) by XREAL_1:232

.= (<%a,b%> . 0) * (q . (i + 1)) by NAT_D:34

.= a * (q . (i + 1)) by POLYNOM5:38 ;

hence (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i)) by A6, A8, A10, A11, Th2; :: thesis: verum