let R be non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr ; for a being Element of R
for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a
let a be Element of R; for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a
let p be FinSequence of the carrier of R; Sum (p * a) = (Sum p) * a
consider f being sequence of the carrier of R such that
A1:
Sum p = f . (len p)
and
A2:
f . 0 = 0. R
and
A3:
for j being Nat
for v being Element of R st j < len p & v = p . (j + 1) holds
f . (j + 1) = (f . j) + v
by RLVECT_1:def 12;
consider fa being sequence of the carrier of R such that
A4:
Sum (p * a) = fa . (len (p * a))
and
A5:
fa . 0 = 0. R
and
A6:
for j being Nat
for v being Element of R st j < len (p * a) & v = (p * a) . (j + 1) holds
fa . (j + 1) = (fa . j) + v
by RLVECT_1:def 12;
defpred S1[ Nat] means (f . $1) * a = fa . $1;
A7: Seg (len (p * a)) =
dom (p * a)
by FINSEQ_1:def 3
.=
dom p
by POLYNOM1:def 2
.=
Seg (len p)
by FINSEQ_1:def 3
;
A8:
now for j being Element of NAT st 0 <= j & j < len p & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 0 <= j & j < len p & S1[j] implies S1[j + 1] )assume that
0 <= j
and A9:
j < len p
;
( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
verumproof
A10:
j < len (p * a)
by A7, A9, FINSEQ_1:6;
then A11:
j + 1
<= len (p * a)
by NAT_1:13;
A12:
0 + 1
<= j + 1
by XREAL_1:6;
then
j + 1
in Seg (len (p * a))
by A11, FINSEQ_1:1;
then
j + 1
in dom (p * a)
by FINSEQ_1:def 3;
then A13:
(p * a) /. (j + 1) = (p * a) . (j + 1)
by PARTFUN1:def 6;
j + 1
in Seg (len p)
by A7, A11, A12, FINSEQ_1:1;
then A14:
j + 1
in dom p
by FINSEQ_1:def 3;
then A15:
p /. (j + 1) = p . (j + 1)
by PARTFUN1:def 6;
assume
(f . j) * a = fa . j
;
S1[j + 1]
hence fa . (j + 1) =
((f . j) * a) + ((p * a) /. (j + 1))
by A6, A10, A13
.=
((f . j) * a) + ((p /. (j + 1)) * a)
by A14, POLYNOM1:def 2
.=
((f . j) + (p /. (j + 1))) * a
by VECTSP_1:def 3
.=
(f . (j + 1)) * a
by A3, A9, A15
;
verum
end; end;
A16:
S1[ 0 ]
by A2, A5, Th1;
A17:
for i being Element of NAT st 0 <= i & i <= len p holds
S1[i]
from INT_1:sch 7(A16, A8);
thus Sum (p * a) =
fa . (len p)
by A4, A7, FINSEQ_1:6
.=
(Sum p) * a
by A1, A17
; verum