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 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 RLVECT_2:def 8;

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 = ZeroLC V by RLVECT_2:def 7;
then Sum L = 0. V by RLVECT_2:48
.= (0. V) + (0. V) by RLVECT_1:10
.= ((0. V) + (0. V)) + (0. V) by RLVECT_1:10
.= ((0 * v1) + (0. V)) + (0. V) by RLVECT_1:23
.= ((0 * v1) + (0 * v2)) + (0. V) by RLVECT_1:23
.= ((0 * v1) + (0 * v2)) + (0 * v3) by RLVECT_1:23
.= (((L . v1) * v1) + (0 * v2)) + (0 * v3) by A3, RLVECT_2:30
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by A3, RLVECT_2:30
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A3, RLVECT_2:30 ;
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 Linear_Combination of {v1} by RLVECT_2:def 8;
A5: ( not v2 in Carrier L & not v3 in Carrier L ) by A1, A4, TARSKI:def 1;
Sum L = (L . v1) * v1 by RLVECT_2:50
.= ((L . v1) * v1) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + (0. V)) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + (0 * v2)) + (0. V) by RLVECT_1:23
.= (((L . v1) * v1) + (0 * v2)) + (0 * v3) by RLVECT_1:23
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by A5, RLVECT_2:28
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A5, RLVECT_2:28 ;
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 Linear_Combination of {v2} by RLVECT_2:def 8;
A7: ( not v1 in Carrier L & not v3 in Carrier L ) by A1, A6, TARSKI:def 1;
Sum L = (L . v2) * v2 by RLVECT_2:50
.= (0. V) + ((L . v2) * v2) by RLVECT_1:10
.= ((0. V) + ((L . v2) * v2)) + (0. V) by RLVECT_1:10
.= ((0 * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:23
.= ((0 * v1) + ((L . v2) * v2)) + (0 * v3) by RLVECT_1:23
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by A7, RLVECT_2:28
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A7, RLVECT_2:28 ;
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 Linear_Combination of {v3} by RLVECT_2:def 8;
A9: ( not v1 in Carrier L & not v2 in Carrier L ) by A1, A8, TARSKI:def 1;
Sum L = (L . v3) * v3 by RLVECT_2:50
.= (0. V) + ((L . v3) * v3) by RLVECT_1:10
.= ((0. V) + (0. V)) + ((L . v3) * v3) by RLVECT_1:10
.= ((0 * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:23
.= ((0 * v1) + (0 * v2)) + ((L . v3) * v3) by RLVECT_1:23
.= (((L . v1) * v1) + (0 * v2)) + ((L . v3) * v3) by A9, RLVECT_2:28
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A9, RLVECT_2:28 ;
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, RLVECT_2:54
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0. V) by RLVECT_1:10
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by RLVECT_1:23 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A11, RLVECT_2:28; :: 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, RLVECT_2:54
.= (((L . v1) * v1) + (0. V)) + ((L . v3) * v3) by RLVECT_1:10
.= (((L . v1) * v1) + (0 * v2)) + ((L . v3) * v3) by RLVECT_1:23 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A13, RLVECT_2:28; :: 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, RLVECT_2:54
.= ((0. V) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:10
.= ((0 * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:23 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by A15, RLVECT_2:28; :: 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 RLVECT_2:def 10;
( 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, 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:44;
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;