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:29;
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 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 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 6;
k in dom p by A1, A2, A5, XBOOLE_0:def 4;
then A8: p /. k = p . k by PARTFUN1:def 6;
k in dom (a * p) by A2, A5, XBOOLE_0:def 4;
then (a * p) . k = a * (p /. k) by A8, FVSUM_1:50;
hence (lmlt ((a * p),R)) . k = (a * (p /. k)) * (R /. k) by A5, A7, FUNCOP_1:22
.= a * ((p /. k) * (R /. k)) by VECTSP_1:def 16
.= a * v1 by A1, A3, A2, A5, A6, A8, A7, FUNCOP_1:22 ;
:: thesis: verum

end;

len (lmlt (p,R)) = len (lmlt ((a * p),R)) by A1, A3, A2, FINSEQ_3:29;
hence Sum (lmlt ((a * p),R)) = a * (Sum (lmlt (p,R))) by A4, RLVECT_2:66; :: thesis: verum