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 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let a be Element of K; :: thesis: for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let V1 be finite-dimensional VectSp of K; :: thesis: for R being FinSequence of V1 holds Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let R be FinSequence of V1; :: thesis: Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
defpred S₁[ Nat] means for R being FinSequence of V1
for a being Element of K st len R = $1 holds
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let R be FinSequence of V1; :: thesis: for a being Element of K st len R = n + 1 holds
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let a be Element of K; :: thesis: ( len R = n + 1 implies Sum (lmlt (((len R) |-> a),R)) = a * (Sum R) )
assume A3: len R = n + 1 ; :: thesis: Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
A4: len (R | n) = n by A3, FINSEQ_1:59, NAT_1:11;
then A5: dom (R | n) = Seg n by FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom R by A3, FINSEQ_3:25;
then A6: R /. (n + 1) = R . (n + 1) by PARTFUN1:def 6;
A7: lmlt (<*a*>,<*(R /. (n + 1))*>) = <*(a * (R /. (n + 1)))*> by FINSEQ_2:74;
A8: ( len <*a*> = 1 & len <*(R . (n + 1))*> = 1 ) by FINSEQ_1:39;
A9: ( (n + 1) |-> a = (n |-> a) ^ <*a*> & len (n |-> a) = n ) by CARD_1:def 7, FINSEQ_2:60;
R = (R | n) ^ <*(R . (n + 1))*> by A3, FINSEQ_3:55;
hence Sum (lmlt (((len R) |-> a),R)) = Sum ((lmlt ((n |-> a),(R | n))) ^ (lmlt (<*a*>,<*(R /. (n + 1))*>))) by A3, A6, A4, A9, A8, Th9
.= (Sum (lmlt ((n |-> a),(R | n)))) + (Sum (lmlt (<*a*>,<*(R /. (n + 1))*>))) by RLVECT_1:41
.= (a * (Sum (R | n))) + (Sum <*(a * (R /. (n + 1)))*>) by A2, A4, A7
.= (a * (Sum (R | n))) + (a * (R /. (n + 1))) by RLVECT_1:44
.= a * ((Sum (R | n)) + (R /. (n + 1))) by VECTSP_1:def 14
.= a * (Sum R) by A3, A6, A4, A5, RLVECT_1:38 ;
:: thesis: verum

end;

A10: S₁[ 0 ]

proof

let R be FinSequence of V1; :: thesis: for a being Element of K st len R = 0 holds
Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
let a be Element of K; :: thesis: ( len R = 0 implies Sum (lmlt (((len R) |-> a),R)) = a * (Sum R) )
assume A11: len R = 0 ; :: thesis: Sum (lmlt (((len R) |-> a),R)) = a * (Sum R)
set L = (len R) |-> a;
set M = lmlt (((len R) |-> a),R);
len ((len R) |-> a) = len R by CARD_1:def 7;
then dom ((len R) |-> a) = dom R by FINSEQ_3:29;
then dom (lmlt (((len R) |-> a),R)) = dom R by MATRLIN:12;
then len R = len (lmlt (((len R) |-> a),R)) by FINSEQ_3:29;
then lmlt (((len R) |-> a),R) = <*> the carrier of V1 by A11;
then A12: Sum (lmlt (((len R) |-> a),R)) = 0. V1 by RLVECT_1:43;
R = <*> the carrier of V1 by A11;
then Sum R = 0. V1 by RLVECT_1:43;
hence Sum (lmlt (((len R) |-> a),R)) = a * (Sum R) by A12, VECTSP_1:14; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A1);
hence Sum (lmlt (((len R) |-> a),R)) = a * (Sum R) ; :: thesis: verum