let K be Field; 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; 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; for p being FinSequence of K holds Sum (lmlt (p,((len p) |-> v1))) = (Sum p) * v1
let p be FinSequence of K; 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 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 * v1let k be
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 * v1let a1 be
Element of
K;
( 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
;
(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;
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; verum