let K be Field; :: thesis: for a being Element of K
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R))
let a be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R))
let V1 be finite-dimensional VectSp of K; :: thesis: for R being FinSequence of V1
for p being FinSequence of K holds Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R))
let R be FinSequence of V1; :: thesis: for p being FinSequence of K holds Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R))
let p be FinSequence of K; :: thesis: Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R))
set Ma = lmlt (a * p),R;
set M = lmlt p,R;
len (a * p) = len p by MATRIXR1:16;
then A1: ( dom (a * p) = dom p & dom (lmlt p,R) = (dom p) /\ (dom R) & dom (lmlt (a * p),R) = (dom (a * p)) /\ (dom R) ) by Lm1, FINSEQ_3:31;
then A2: len (lmlt p,R) = len (lmlt (a * p),R) by FINSEQ_3:31;
for k being Element of NAT
for v1 being Element of V1 st k in dom (lmlt (a * p),R) & v1 = (lmlt p,R) . k holds
(lmlt (a * p),R) . k = a * v1

proof

let k be Element of NAT ; :: thesis: for v1 being Element of V1 st k in dom (lmlt (a * p),R) & v1 = (lmlt p,R) . k holds
(lmlt (a * p),R) . k = a * v1
let v1 be Element of V1; :: thesis: ( k in dom (lmlt (a * p),R) & v1 = (lmlt p,R) . k implies (lmlt (a * p),R) . k = a * v1 )
assume A3: ( k in dom (lmlt (a * p),R) & v1 = (lmlt p,R) . k ) ; :: thesis: (lmlt (a * p),R) . k = a * v1
A4: ( k in dom p & k in dom R & k in dom (a * p) ) by A1, A3, XBOOLE_0:def 4;
then A5: ( p /. k = p . k & R /. k = R . k ) by PARTFUN1:def 8;
then (a * p) . k = a * (p /. k) by A4, FVSUM_1:62;
hence (lmlt (a * p),R) . k = (a * (p /. k)) * (R /. k) by A5, A3, FUNCOP_1:28
.= a * ((p /. k) * (R /. k)) by VECTSP_1:def 26
.= a * v1 by A5, A1, A3, FUNCOP_1:28 ;
:: thesis: verum

end;

hence Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R)) by A2, VECTSP_3:9; :: thesis: verum