let V be ComplexLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V
for L being C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
let v1, v2, v3 be VECTOR of V; :: thesis: for L being C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
let L be C_Linear_Combination of {v1,v2,v3}; :: thesis: ( v1 <> v2 & v2 <> v3 & v3 <> v1 implies Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1 ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
A4: Carrier L c= {v1,v2,v3} by Def4;

per cases ( Carrier L = {} or Carrier L = {v1} or Carrier L = {v2} or Carrier L = {v3} or Carrier L = {v1,v2} or Carrier L = {v1,v3} or Carrier L = {v2,v3} or Carrier L = {v1,v2,v3} ) by A4, ZFMISC_1:118;

suppose Carrier L = {} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then A5: L = ZeroCLC V by Def3;
then Sum L = 0. V by Th11
.= (0. V) + (0. V)
.= ((0. V) + (0. V)) + (0. V)
.= ((0c * v1) + (0. V)) + (0. V) by CLVECT_1:1
.= ((0c * v1) + (0c * v2)) + (0. V) by CLVECT_1:1
.= ((0c * v1) + (0c * v2)) + (0c * v3) by CLVECT_1:1
.= (((L . v1) * v1) + (0c * v2)) + (0c * v3) by A5, Th2
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A5, Th2
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A5, Th2 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A6: Carrier L = {v1} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then reconsider L = L as C_Linear_Combination of {v1} by Def4;
A7: not v2 in Carrier L by A1, A6, TARSKI:def 1;
A8: not v3 in Carrier L by A3, A6, TARSKI:def 1;
Sum L = (L . v1) * v1 by Th14
.= ((L . v1) * v1) + (0. V)
.= (((L . v1) * v1) + (0. V)) + (0. V)
.= (((L . v1) * v1) + (0c * v2)) + (0. V) by CLVECT_1:1
.= (((L . v1) * v1) + (0c * v2)) + (0c * v3) by CLVECT_1:1
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A7
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A8 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A9: Carrier L = {v2} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then reconsider L = L as C_Linear_Combination of {v2} by Def4;
A10: not v1 in Carrier L by A1, A9, TARSKI:def 1;
A11: not v3 in Carrier L by A2, A9, TARSKI:def 1;
Sum L = (L . v2) * v2 by Th14
.= (0. V) + ((L . v2) * v2)
.= ((0. V) + ((L . v2) * v2)) + (0. V)
.= ((0c * v1) + ((L . v2) * v2)) + (0. V) by CLVECT_1:1
.= ((0c * v1) + ((L . v2) * v2)) + (0c * v3) by CLVECT_1:1
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A10
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A11 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A12: Carrier L = {v3} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then reconsider L = L as C_Linear_Combination of {v3} by Def4;
A13: not v1 in Carrier L by A3, A12, TARSKI:def 1;
A14: not v2 in Carrier L by A2, A12, TARSKI:def 1;
Sum L = (L . v3) * v3 by Th14
.= (0. V) + ((L . v3) * v3)
.= ((0. V) + (0. V)) + ((L . v3) * v3)
.= ((0c * v1) + (0. V)) + ((L . v3) * v3) by CLVECT_1:1
.= ((0c * v1) + (0c * v2)) + ((L . v3) * v3) by CLVECT_1:1
.= (((L . v1) * v1) + (0c * v2)) + ((L . v3) * v3) by A13
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A14 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A15: Carrier L = {v1,v2} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then A16: Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A1, Th18
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V)
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by CLVECT_1:1 ;
not v3 in Carrier L by A2, A3, A15, TARSKI:def 2;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A16; :: thesis: verum

end;

suppose A17: Carrier L = {v1,v3} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then A18: Sum L = ((L . v1) * v1) + ((L . v3) * v3) by A3, Th18
.= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3)
.= (((L . v1) * v1) + (0c * v2)) + ((L . v3) * v3) by CLVECT_1:1 ;
not v2 in Carrier L by A1, A2, A17, TARSKI:def 2;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A18; :: thesis: verum

end;

suppose A19: Carrier L = {v2,v3} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then A20: Sum L = ((L . v2) * v2) + ((L . v3) * v3) by A2, Th18
.= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3)
.= ((0c * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by CLVECT_1:1 ;
not v1 in Carrier L by A1, A3, A19, TARSKI:def 2;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A20; :: thesis: verum

end;

suppose Carrier L = {v1,v2,v3} ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)

then consider F being FinSequence of the carrier of V such that
A21: ( F is one-to-one & rng F = {v1,v2,v3} ) and
A22: Sum L = Sum (L (#) F) by Def6;
( F = <*v1,v2,v3*> or F = <*v1,v3,v2*> or F = <*v2,v1,v3*> or F = <*v2,v3,v1*> or F = <*v3,v1,v2*> or F = <*v3,v2,v1*> ) by A1, A2, A3, A21, CONVEX1:31;
then ( L (#) F = <*((L . v1) * v1),((L . v2) * v2),((L . v3) * v3)*> or L (#) F = <*((L . v1) * v1),((L . v3) * v3),((L . v2) * v2)*> or L (#) F = <*((L . v2) * v2),((L . v1) * v1),((L . v3) * v3)*> or L (#) F = <*((L . v2) * v2),((L . v3) * v3),((L . v1) * v1)*> or L (#) F = <*((L . v3) * v3),((L . v1) * v1),((L . v2) * v2)*> or L (#) F = <*((L . v3) * v3),((L . v2) * v2),((L . v1) * v1)*> ) by Th10;
then ( Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) or Sum L = ((L . v1) * v1) + (((L . v2) * v2) + ((L . v3) * v3)) or Sum L = ((L . v2) * v2) + (((L . v1) * v1) + ((L . v3) * v3)) ) by A22, RLVECT_1:46;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:def 3; :: thesis: verum

end;

end;