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 CARD_1:def 7;
then dom ((len p) |-> v1) = dom p by FINSEQ_3:29;
then A1: dom (lmlt (p,((len p) |-> v1))) = dom p by MATRLIN:12;
A2: now :: thesis: for k being Nat
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 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 that
A3: k in dom (lmlt (p,((len p) |-> v1))) and
A4: 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:57;
hence (lmlt (p,((len p) |-> v1))) . k = a1 * v1 by A3, A4, FUNCOP_1:22; :: thesis: verum
end;
len p = len (lmlt (p,((len p) |-> v1))) by A1, FINSEQ_3:29;
hence Sum (lmlt (p,((len p) |-> v1))) = (Sum p) * v1 by A2, MATRLIN:9; :: thesis: verum