let R be non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr ; :: thesis: for a being Element of R
for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)
let a be Element of R; :: thesis: for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)
let p be FinSequence of the carrier of R; :: thesis: Sum (a * p) = a * (Sum p)
consider f being Function of NAT ,the carrier of R such that
A1:
( Sum p = f . (len p) & f . 0 = 0. R & ( for j being Element of 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 13;
consider fa being Function of NAT ,the carrier of R such that
A2:
( Sum (a * p) = fa . (len (a * p)) & fa . 0 = 0. R & ( for j being Element of NAT
for v being Element of R st j < len (a * p) & v = (a * p) . (j + 1) holds
fa . (j + 1) = (fa . j) + v ) )
by RLVECT_1:def 13;
A3: Seg (len (a * p)) =
dom (a * p)
by FINSEQ_1:def 3
.=
dom p
by POLYNOM1:def 2
.=
Seg (len p)
by FINSEQ_1:def 3
;
defpred S1[ Element of NAT ] means a * (f . $1) = fa . $1;
A4:
S1[ 0 ]
by A1, A2, Th2;
A5:
now let j be
Element of
NAT ;
:: thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] )assume A6:
(
0 <= j &
j < len p )
;
:: thesis: ( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
:: thesis: verumproof
assume A7:
S1[
j]
;
:: thesis: S1[j + 1]
A8:
j < len (a * p)
by A3, A6, FINSEQ_1:8;
then A9:
j + 1
<= len (a * p)
by NAT_1:13;
A10:
j + 1
<= len p
by A6, NAT_1:13;
A11:
0 + 1
<= j + 1
by XREAL_1:8;
then
j + 1
in Seg (len (a * p))
by A9, FINSEQ_1:3;
then
j + 1
in dom (a * p)
by FINSEQ_1:def 3;
then A12:
(a * p) /. (j + 1) = (a * p) . (j + 1)
by PARTFUN1:def 8;
j + 1
in Seg (len p)
by A10, A11, FINSEQ_1:3;
then A13:
j + 1
in dom p
by FINSEQ_1:def 3;
then A14:
p /. (j + 1) = p . (j + 1)
by PARTFUN1:def 8;
thus fa . (j + 1) =
(a * (f . j)) + ((a * p) /. (j + 1))
by A2, A7, A8, A12
.=
(a * (f . j)) + (a * (p /. (j + 1)))
by A13, POLYNOM1:def 2
.=
a * ((f . j) + (p /. (j + 1)))
by VECTSP_1:def 11
.=
a * (f . (j + 1))
by A1, A6, A14
;
:: thesis: verum
end; end;
A15:
for i being Element of NAT st 0 <= i & i <= len p holds
S1[i]
from POLYNOM2:sch 4(A4, A5);
thus Sum (a * p) =
fa . (len p)
by A2, A3, FINSEQ_1:8
.=
a * (Sum p)
by A1, A15
; :: thesis: verum