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;

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) * vend;

hence
Sum l = (l . v) * v
; :: thesis: verumper cases
( Carrier l = {} or Carrier l = {v} )
by A1, ZFMISC_1:33;

end;

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 A2, Th3 ;

:: thesis: verum

end;hence Sum l = 0. V by Lm1

.= (0. GF) * v by VECTSP_1:14

.= (l . v) * v by A2, Th3 ;

:: thesis: verum

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 A3, FINSEQ_3:97;

then l (#) F = <*((l . v) * v)*> by Th10;

hence Sum l = (l . v) * v by A4, RLVECT_1:44; :: thesis: verum

end;A3: ( F is one-to-one & rng F = {v} ) and

A4: Sum l = Sum (l (#) F) by Def6;

F = <*v*> by A3, FINSEQ_3:97;

then l (#) F = <*((l . v) * v)*> by Th10;

hence Sum l = (l . v) * v by A4, RLVECT_1:44; :: thesis: verum