let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for v1 being Element of V1
for p being FinSequence of K holds Sum (lmlt p,((len p) |-> v1)) = (Sum p) * v1
let V1 be finite-dimensional VectSp of K; :: thesis: for v1 being Element of V1
for p being FinSequence of K holds Sum (lmlt p,((len p) |-> v1)) = (Sum p) * v1
let v1 be Element of V1; :: thesis: for p being FinSequence of K holds Sum (lmlt p,((len p) |-> v1)) = (Sum p) * v1
let p be FinSequence of K; :: thesis: Sum (lmlt p,((len p) |-> v1)) = (Sum p) * v1
set L = (len p) |-> v1;
set M = lmlt p,((len p) |-> v1);
len ((len p) |-> v1) = len p by FINSEQ_1:def 18;
then dom ((len p) |-> v1) = dom p by FINSEQ_3:31;
then A1: dom (lmlt p,((len p) |-> v1)) = dom p by MATRLIN:16;
then A2: len p = len (lmlt p,((len p) |-> v1)) by FINSEQ_3:31;

now

let k be Nat; :: thesis: for a1 being Element of K st k in dom (lmlt p,((len p) |-> v1)) & a1 = p . k holds
(lmlt p,((len p) |-> v1)) . k = a1 * v1
let a1 be Element of K; :: thesis: ( k in dom (lmlt p,((len p) |-> v1)) & a1 = p . k implies (lmlt p,((len p) |-> v1)) . k = a1 * v1 )
assume A3: ( k in dom (lmlt p,((len p) |-> v1)) & a1 = p . k ) ; :: thesis: (lmlt p,((len p) |-> v1)) . k = a1 * v1
k in Seg (len p) by A1, A3, FINSEQ_1:def 3;
then ((len p) |-> v1) . k = v1 by FINSEQ_2:71;
hence (lmlt p,((len p) |-> v1)) . k = a1 * v1 by A3, FUNCOP_1:28; :: thesis: verum

end;

hence Sum (lmlt p,((len p) |-> v1)) = (Sum p) * v1 by A2, MATRLIN:13; :: thesis: verum