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 ;
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
.= (((L . v1) * v1) + ((L . v2) * v2)) + (0 * v3) by
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ;
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 ;
A8: not v3 in Carrier L by ;
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
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ;
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 ;
A11: not v3 in Carrier L by ;
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
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ;
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 ;
A14: not v2 in Carrier L by ;
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
.= (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ;
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
.= (((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 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ; :: 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
.= (((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 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ; :: 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
.= ((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 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by ; :: 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 ;
hence Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) by RLVECT_1:def 3; :: thesis: verum
end;
end;