let GF be Ring; :: thesis: for V being LeftMod of GF
for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L)
let V be LeftMod of GF; :: thesis: for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; :: thesis: for a being Scalar of holds Sum (a * L) = a * (Sum L)
let a be Scalar of GF; :: thesis: Sum (a * L) = a * (Sum L)
set l = a * L;
Carrier (a * L) c= Carrier L by VECTSP_6:28;
then consider F being FinSequence of the carrier of V such that
A1: ( F is one-to-one & rng F = Carrier L ) and
A2: Sum (a * L) = Sum ((a * L) (#) F) by TH2;
set f = (a * L) (#) F;
set g = L (#) F;
A3: len ((a * L) (#) F) = len F by VECTSP_6:def 5
.= len (L (#) F) by VECTSP_6:def 5 ;
len ((a * L) (#) F) = len F by VECTSP_6:def 5;
then A4: dom F = Seg (len ((a * L) (#) F)) by FINSEQ_1:def 3;

A5: now :: thesis: for k being Nat
for v being Vector of V st k in dom ((a * L) (#) F) & v = (L (#) F) . k holds
((a * L) (#) F) . k = a * v

let k be Nat; :: thesis: for v being Vector of V st k in dom ((a * L) (#) F) & v = (L (#) F) . k holds
((a * L) (#) F) . k = a * v
let v be Vector of V; :: thesis: ( k in dom ((a * L) (#) F) & v = (L (#) F) . k implies ((a * L) (#) F) . k = a * v )
assume that
A6: k in dom ((a * L) (#) F) and
A7: v = (L (#) F) . k ; :: thesis: ((a * L) (#) F) . k = a * v
set v9 = F /. k;
A8: k in Seg (len ((a * L) (#) F)) by A6, FINSEQ_1:def 3;
then A9: F /. k = F . k by A4, PARTFUN1:def 6;
hence ((a * L) (#) F) . k = ((a * L) . (F /. k)) * (F /. k) by A4, A8, VECTSP_6:8
.= (a * (L . (F /. k))) * (F /. k) by VECTSP_6:def 9
.= a * ((L . (F /. k)) * (F /. k)) by VECTSP_1:def 16
.= a * v by A4, A7, A8, A9, VECTSP_6:8 ;
:: thesis: verum

end;

Sum L = Sum (L (#) F) by A1, VECTSP_6:def 6;
hence Sum (a * L) = a * (Sum L) by A2, A3, A5, RLVECT_2:66; :: thesis: verum