let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)
let V be RightMod of R; :: thesis: for v being Vector of V
for l being Linear_Combination of {v} holds Sum l = v * (l . v)
let v be Vector of V; :: thesis: for l being Linear_Combination of {v} holds Sum l = v * (l . v)
let l be Linear_Combination of {v}; :: thesis: Sum l = v * (l . v)
A1: Carrier l c= {v} by Def5;

now :: thesis: Sum l = v * (l . v)

per cases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33;

suppose Carrier l = {} ; :: thesis: Sum l = v * (l . v)

then A2: l = ZeroLC V by Def4;
hence Sum l = 0. V by Lm3
.= v * (0. R) by VECTSP_2:32
.= v * (l . v) by A2, Th18 ;
:: thesis: verum

end;

suppose Carrier l = {v} ; :: thesis: Sum l = v * (l . v)

then consider F being FinSequence of V such that
A3: ( F is one-to-one & rng F = {v} ) and
A4: Sum l = Sum (l (#) F) by Def7;
F = <*v*> by A3, FINSEQ_3:97;
then l (#) F = <*(v * (l . v))*> by Th25;
hence Sum l = v * (l . v) by A4, RLVECT_1:44; :: thesis: verum

end;

end;

end;

hence Sum l = v * (l . v) ; :: thesis: verum