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: 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 A2: 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 FINSEQ_1:def 18;
then dom ((len R) |-> a) = dom R by FINSEQ_3:31;
then dom (lmlt ((len R) |-> a),R) = dom R by MATRLIN:16;
then len R = len (lmlt ((len R) |-> a),R) by FINSEQ_3:31;
then ( R = <*> the carrier of V1 & lmlt ((len R) |-> a),R = <*> the carrier of V1 ) by A2;
then ( Sum R = 0. V1 & Sum (lmlt ((len R) |-> a),R) = 0. V1 ) by RLVECT_1:60;
hence Sum (lmlt ((len R) |-> a),R) = a * (Sum R) by VECTSP_1:59; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: 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 A5: len R = n + 1 ; :: thesis: Sum (lmlt ((len R) |-> a),R) = a * (Sum R)
1 <= n + 1 by NAT_1:11;
then n + 1 in dom R by A5, FINSEQ_3:27;
then A6: ( R /. (n + 1) = R . (n + 1) & R = (R | n) ^ <*(R . (n + 1))*> & (n + 1) |-> a = (n |-> a) ^ <*a*> ) by A5, FINSEQ_2:74, FINSEQ_3:61, PARTFUN1:def 8;
n <= n + 1 by NAT_1:11;
then A7: ( len (R | n) = n & len (n |-> a) = n & len <*a*> = 1 & len <*(R . (n + 1))*> = 1 ) by A5, FINSEQ_1:56, FINSEQ_1:80, FINSEQ_1:def 18;
A8: lmlt <*a*>,<*(R /. (n + 1))*> = <*(a * (R /. (n + 1)))*> by FINSEQ_2:88;
A9: dom (R | n) = Seg n by A7, FINSEQ_1:def 3;
thus Sum (lmlt ((len R) |-> a),R) = Sum ((lmlt (n |-> a),(R | n)) ^ (lmlt <*a*>,<*(R /. (n + 1))*>)) by A5, A6, A7, Th9
.= (Sum (lmlt (n |-> a),(R | n))) + (Sum (lmlt <*a*>,<*(R /. (n + 1))*>)) by RLVECT_1:58
.= (a * (Sum (R | n))) + (Sum <*(a * (R /. (n + 1)))*>) by A4, A7, A8
.= (a * (Sum (R | n))) + (a * (R /. (n + 1))) by RLVECT_1:61
.= a * ((Sum (R | n)) + (R /. (n + 1))) by VECTSP_1:def 26
.= a * (Sum R) by A5, A6, A7, A9, RLVECT_1:55 ; :: thesis: verum

end;

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