let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v being Element of V
for l being Linear_Combination of {v} holds Sum l = (l . v) * v

let v be Element of V; :: thesis: for l being Linear_Combination of {v} holds Sum l = (l . v) * v
let l be Linear_Combination of {v}; :: thesis: Sum l = (l . v) * v
A1: Carrier l c= {v} by Def4;
now :: thesis: Sum l = (l . v) * v
per cases ( Carrier l = {} or Carrier l = {v} ) by ;
suppose Carrier l = {} ; :: thesis: Sum l = (l . v) * v
then A2: l = ZeroLC V by Def3;
hence Sum l = 0. V by Lm1
.= (0. GF) * v by VECTSP_1:14
.= (l . v) * v by ;
:: thesis: verum
end;
suppose Carrier l = {v} ; :: thesis: Sum l = (l . v) * 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 Def6;
F = <*v*> by ;
then l (#) F = <*((l . v) * v)*> by Th10;
hence Sum l = (l . v) * v by ; :: thesis: verum
end;
end;
end;
hence Sum l = (l . v) * v ; :: thesis: verum