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 ;

A11: now :: thesis: for k being Element of NAT st 2 < k & k in dom r holds
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;

1 <= len r by A8, XXREAL_0:2;
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