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 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 (a * p) = fa . (len (a * p)) and
A5: fa . 0 = 0. R and
A6: for j being 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 12;
defpred S₁[ Nat] means a * (f . $1) = fa . $1;
A7: Seg (len (a * p)) = dom (a * p) by FINSEQ_1:def 3
.= dom p by POLYNOM1:def 1
.= Seg (len p) by FINSEQ_1:def 3 ;

A8: now :: thesis: for j being Element of NAT st 0 <= j & j < len p & S₁[j] holds
S₁[j + 1]

let j be Element of NAT ; :: thesis: ( 0 <= j & j < len p & S₁[j] implies S₁[j + 1] )
assume that
0 <= j and
A9: j < len p ; :: thesis: ( S₁[j] implies S₁[j + 1] )
thus ( S₁[j] implies S₁[j + 1] ) :: thesis: verum

proof

A10: 0 + 1 <= j + 1 by XREAL_1:6;
A11: j < len (a * p) by A7, A9, FINSEQ_1:6;
then j + 1 <= len (a * p) by NAT_1:13;
then j + 1 in Seg (len (a * p)) by A10, FINSEQ_1:1;
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 6;
j + 1 <= len p by A9, NAT_1:13;
then j + 1 in Seg (len p) by A10, FINSEQ_1:1;
then A13: j + 1 in dom p by FINSEQ_1:def 3;
then A14: p /. (j + 1) = p . (j + 1) by PARTFUN1:def 6;
assume S₁[j] ; :: thesis: S₁[j + 1]
hence fa . (j + 1) = (a * (f . j)) + ((a * p) /. (j + 1)) by A6, A11, A12
.= (a * (f . j)) + (a * (p /. (j + 1))) by A13, POLYNOM1:def 1
.= a * ((f . j) + (p /. (j + 1))) by VECTSP_1:def 2
.= a * (f . (j + 1)) by A3, A9, A14 ;
:: thesis: verum

end;

end;

A15: S₁[ 0 ] by A2, A5, Th2;
A16: for i being Element of NAT st 0 <= i & i <= len p holds
S₁[i] from INT_1:sch 7(A15, A8);
thus Sum (a * p) = fa . (len p) by A4, A7, FINSEQ_1:6
.= a * (Sum p) by A1, A16 ; :: thesis: verum