let R be Ring; :: thesis: for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let V be LeftMod of R; :: thesis: for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; :: thesis: for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let a be Scalar of R; :: thesis: Sum (a * L) = a * (Sum L)
set l = a * L;
Carrier (a * L) c= Carrier L by VECTSP_6:58;
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 Th6;
set f = (a * L) (#) F;
set g = L (#) F;
A3: len ((a * L) (#) F) = len F by VECTSP_6:def 8
.= len (L (#) F) by VECTSP_6:def 8 ;
len ((a * L) (#) F) = len F by VECTSP_6:def 8;
then A4: dom F = Seg (len ((a * L) (#) F)) by FINSEQ_1:def 3;

A5: now

let k be Element of 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 8;
hence ((a * L) (#) F) . k = ((a * L) . (F /. k)) * (F /. k) by A4, A8, VECTSP_6:32
.= (a * (L . (F /. k))) * (F /. k) by VECTSP_6:def 12
.= a * ((L . (F /. k)) * (F /. k)) by VECTSP_1:def 26
.= a * v by A4, A7, A8, A9, VECTSP_6:32 ;
:: thesis: verum

end;

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