let V be RealLinearSpace; :: thesis: for v1, v2, v3 being VECTOR of V
for L being 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 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 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 RLVECT_2:def 6;

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 = ZeroLC V by RLVECT_2:def 5;
then Sum L = 0. V by RLVECT_2:30
.= (0. V) + (0. V)
.= ((0. V) + (0. V)) + (0. V)
.= ((0 * v1) + (0. V)) + (0. V) by RLVECT_1:10
.= ((0 * v1) + (0 * v2)) + (0. V) by RLVECT_1:10
.= ((0 * v1) + (0 * v2)) + (0 * v3) by RLVECT_1:10
.= (((L . v1) * v1) + (0 * v2)) + (0 * v3) by A5, RLVECT_2:20
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by A5, RLVECT_2:20
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A5, RLVECT_2:20 ;
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 Linear_Combination of {v1} by RLVECT_2:def 6;
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 RLVECT_2:32
.= ((L . v1) * v1) + (0. V)
.= (((L . v1) * v1) + (0. V)) + (0. V)
.= (((L . v1) * v1) + (0 * v2)) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + (0 * v2)) + (0 * v3) by RLVECT_1:10
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by A7, RLVECT_2:19
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A8, RLVECT_2:19 ;
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 Linear_Combination of {v2} by RLVECT_2:def 6;
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 RLVECT_2:32
.= (0. V) + ((L . v2) * v2)
.= ((0. V) + ((L . v2) * v2)) + (0. V)
.= ((0 * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:10
.= ((0 * v1) + ((L . v2) * v2)) + (0 * v3) by RLVECT_1:10
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by A10, RLVECT_2:19
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A11, RLVECT_2:19 ;
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 Linear_Combination of {v3} by RLVECT_2:def 6;
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 RLVECT_2:32
.= (0. V) + ((L . v3) * v3)
.= ((0. V) + (0. V)) + ((L . v3) * v3)
.= ((0 * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:10
.= ((0 * v1) + (0 * v2)) + ((L . v3) * v3) by RLVECT_1:10
.= (((L . v1) * v1) + (0 * v2)) + ((L . v3) * v3) by A13, RLVECT_2:19
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A14, RLVECT_2:19 ;
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, RLVECT_2:36
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V)
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by RLVECT_1:10 ;
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, RLVECT_2:19; :: 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, RLVECT_2:36
.= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3)
.= (((L . v1) * v1) + (0 * v2)) + ((L . v3) * v3) by RLVECT_1:10 ;
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, RLVECT_2:19; :: 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, RLVECT_2:36
.= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3)
.= ((0 * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:10 ;
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, RLVECT_2:19; :: 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 RLVECT_2:def 8;
( 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, Lm13;
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 RLVECT_2:28;
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;