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 by FINSEQ_3:31;
A2: dom (lmlt (a * p),R) = (dom (a * p)) /\ (dom R) by Lm1;
A3: dom (lmlt p,R) = (dom p) /\ (dom R) by Lm1;
A4: 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 that
A5: k in dom (lmlt (a * p),R) and
A6: v1 = (lmlt p,R) . k ; :: thesis: (lmlt (a * p),R) . k = a * v1
k in dom R by A2, A5, XBOOLE_0:def 4;
then A7: R /. k = R . k by PARTFUN1:def 8;
k in dom p by A1, A2, A5, XBOOLE_0:def 4;
then A8: p /. k = p . k by PARTFUN1:def 8;
k in dom (a * p) by A2, A5, XBOOLE_0:def 4;
then (a * p) . k = a * (p /. k) by A8, FVSUM_1:62;
hence (lmlt (a * p),R) . k = (a * (p /. k)) * (R /. k) by A5, A7, FUNCOP_1:28
.= a * ((p /. k) * (R /. k)) by VECTSP_1:def 28
.= a * v1 by A1, A3, A2, A5, A6, A8, A7, FUNCOP_1:28 ;
:: thesis: verum

end;

len (lmlt p,R) = len (lmlt (a * p),R) by A1, A3, A2, FINSEQ_3:31;
hence Sum (lmlt (a * p),R) = a * (Sum (lmlt p,R)) by A4, VECTSP_3:9; :: thesis: verum