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 A1: ( v1 <> v2 & v2 <> v3 & v3 <> v1 ) ; :: thesis: Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
A2: Carrier L c= {v1,v2,v3} by Def3;

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 A2, ZFMISC_1:142;

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

then A3: L = ZeroCLC V by Def2;
then Sum L = 0. V by Lm2
.= (0. V) + (0. V) by RLVECT_1:10
.= ((0. V) + (0. V)) + (0. V) by RLVECT_1:10
.= ((0c * v1) + (0. V)) + (0. V) by CLVECT_1:2
.= ((0c * v1) + (0c * v2)) + (0. V) by CLVECT_1:2
.= ((0c * v1) + (0c * v2)) + (0c * v3) by CLVECT_1:2
.= (((L . v1) * v1) + (0c * v2)) + (0c * v3) by A3, Th30
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A3, Th30
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A3, Th30 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A4: 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 Def3;
A5: ( not v2 in Carrier L & not v3 in Carrier L ) by A1, A4, TARSKI:def 1;
Sum L = (L . v1) * v1 by Th50
.= ((L . v1) * v1) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + (0. V)) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + (0c * v2)) + (0. V) by CLVECT_1:2
.= (((L . v1) * v1) + (0c * v2)) + (0c * v3) by CLVECT_1:2
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A5
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A5 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A6: 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 Def3;
A7: ( not v1 in Carrier L & not v3 in Carrier L ) by A1, A6, TARSKI:def 1;
Sum L = (L . v2) * v2 by Th50
.= (0. V) + ((L . v2) * v2) by RLVECT_1:10
.= ((0. V) + ((L . v2) * v2)) + (0. V) by RLVECT_1:10
.= ((0c * v1) + ((L . v2) * v2)) + (0. V) by CLVECT_1:2
.= ((0c * v1) + ((L . v2) * v2)) + (0c * v3) by CLVECT_1:2
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by A7
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A7 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

suppose A8: 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 Def3;
A9: ( not v1 in Carrier L & not v2 in Carrier L ) by A1, A8, TARSKI:def 1;
Sum L = (L . v3) * v3 by Th50
.= (0. V) + ((L . v3) * v3) by RLVECT_1:10
.= ((0. V) + (0. V)) + ((L . v3) * v3) by RLVECT_1:10
.= ((0c * v1) + (0. V)) + ((L . v3) * v3) by CLVECT_1:2
.= ((0c * v1) + (0c * v2)) + ((L . v3) * v3) by CLVECT_1:2
.= (((L . v1) * v1) + (0c * v2)) + ((L . v3) * v3) by A9
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A9 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ; :: thesis: verum

end;

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

then A11: not v3 in Carrier L by A1, TARSKI:def 2;
Sum L = ((L . v1) * v1) + ((L . v2) * v2) by A1, A10, Th54
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0c * v3) by CLVECT_1:2 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A11; :: thesis: verum

end;

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

then A13: not v2 in Carrier L by A1, TARSKI:def 2;
Sum L = ((L . v1) * v1) + ((L . v3) * v3) by A1, A12, Th54
.= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:10
.= (((L . v1) * v1) + (0c * v2)) + ((L . v3) * v3) by CLVECT_1:2 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A13; :: thesis: verum

end;

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

then A15: not v1 in Carrier L by A1, TARSKI:def 2;
Sum L = ((L . v2) * v2) + ((L . v3) * v3) by A1, A14, Th54
.= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:10
.= ((0c * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by CLVECT_1:2 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A15; :: 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
A16: ( F is one-to-one & rng F = {v1,v2,v3} ) and
A17: Sum L = Sum (L (#) F) by Def5;
( 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, A16, 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 Th44;
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 A17, RLVECT_1:63;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:def 6; :: thesis: verum

end;

end;