let R be Ring; :: thesis: for V being RightMod of R
for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
let V be RightMod of R; :: thesis: for v1, v2 being Vector of V st v1 <> v2 holds
for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
let v1, v2 be Vector of V; :: thesis: ( v1 <> v2 implies for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) )
assume A1: v1 <> v2 ; :: thesis: for l being Linear_Combination of {v1,v2} holds Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
let l be Linear_Combination of {v1,v2}; :: thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))
A2: Carrier l c= {v1,v2} by Def5;

now :: thesis: Sum l = (v1 * (l . v1)) + (v2 * (l . v2))

per cases ( Carrier l = {} or Carrier l = {v1} or Carrier l = {v2} or Carrier l = {v1,v2} ) by A2, ZFMISC_1:36;

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

then A3: l = ZeroLC V by Def4;
hence Sum l = 0. V by Lm3
.= (0. V) + (0. V) by RLVECT_1:def 4
.= (v1 * (0. R)) + (0. V) by VECTSP_2:32
.= (v1 * (0. R)) + (v2 * (0. R)) by VECTSP_2:32
.= (v1 * (l . v1)) + (v2 * (0. R)) by A3, Th18
.= (v1 * (l . v1)) + (v2 * (l . v2)) by A3, Th18 ;
:: thesis: verum

end;

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

then reconsider L = l as Linear_Combination of {v1} by Def5;
A5: not v2 in Carrier l by A1, A4, TARSKI:def 1;
thus Sum l = Sum L
.= v1 * (l . v1) by Th32
.= (v1 * (l . v1)) + (0. V) by RLVECT_1:def 4
.= (v1 * (l . v1)) + (v2 * (0. R)) by VECTSP_2:32
.= (v1 * (l . v1)) + (v2 * (l . v2)) by A5 ; :: thesis: verum

end;

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

then reconsider L = l as Linear_Combination of {v2} by Def5;
A7: not v1 in Carrier l by A1, A6, TARSKI:def 1;
thus Sum l = Sum L
.= v2 * (l . v2) by Th32
.= (0. V) + (v2 * (l . v2)) by RLVECT_1:def 4
.= (v1 * (0. R)) + (v2 * (l . v2)) by VECTSP_2:32
.= (v1 * (l . v1)) + (v2 * (l . v2)) by A7 ; :: thesis: verum

end;

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

then consider F being FinSequence of V such that
A8: ( F is one-to-one & rng F = {v1,v2} ) and
A9: Sum l = Sum (l (#) F) by Def7;
( F = <*v1,v2*> or F = <*v2,v1*> ) by A1, A8, FINSEQ_3:99;
then ( l (#) F = <*(v1 * (l . v1)),(v2 * (l . v2))*> or l (#) F = <*(v2 * (l . v2)),(v1 * (l . v1))*> ) by Th26;
hence Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) by A9, RLVECT_1:45; :: thesis: verum

end;

end;

end;

hence Sum l = (v1 * (l . v1)) + (v2 * (l . v2)) ; :: thesis: verum