let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; 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; 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; ( (<%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; for i being Nat holds (<%a,b%> *' q) . (i + 1) = (a * (q . (i + 1))) + (b * (q . i))
let i be Nat; (<%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
;
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; verum