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:80, 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:27;
then A6: R /. (n + 1) = R . (n + 1) by PARTFUN1:def 8;
A7: lmlt <*a*>,<*(R /. (n + 1))*> = <*(a * (R /. (n + 1)))*> by FINSEQ_2:88;
A8: ( len <*a*> = 1 & len <*(R . (n + 1))*> = 1 ) by FINSEQ_1:56;
A9: ( (n + 1) |-> a = (n |-> a) ^ <*a*> & len (n |-> a) = n ) by FINSEQ_1:def 18, FINSEQ_2:74;
R = (R | n) ^ <*(R . (n + 1))*> by A3, FINSEQ_3:61;
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:58
.= (a * (Sum (R | n))) + (Sum <*(a * (R /. (n + 1)))*>) by A2, A4, A7
.= (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 A3, A6, A4, A5, RLVECT_1:55 ;
:: 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 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 lmlt ((len R) |-> a),R = <*> the carrier of V1 by A11;
then A12: Sum (lmlt ((len R) |-> a),R) = 0. V1 by RLVECT_1:60;
R = <*> the carrier of V1 by A11;
then Sum R = 0. V1 by RLVECT_1:60;
hence Sum (lmlt ((len R) |-> a),R) = a * (Sum R) by A12, VECTSP_1:59; :: 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