let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V
for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v
let v be VECTOR of V; :: thesis: for l being C_Linear_Combination of {v} holds Sum l = (l . v) * v
let l be C_Linear_Combination of {v}; :: thesis: Sum l = (l . v) * v
A1: Carrier l c= {v} by Def4;
per cases ( Carrier l = {} or Carrier l = {v} ) by A1, ZFMISC_1:33;
suppose Carrier l = {} ; :: thesis: Sum l = (l . v) * v
then A2: l = ZeroCLC V by Def3;
hence Sum l = 0. V by Th11
.= 0c * v by CLVECT_1:1
.= (l . v) * v by A2, Th2 ;
:: thesis: verum
end;
suppose Carrier l = {v} ; :: thesis: Sum l = (l . v) * v
then consider F being FinSequence of the carrier 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 Th8;
hence Sum l = (l . v) * v by A4, RLVECT_1:44; :: thesis: verum
end;
end;