theorem :: ZMODUL02:25

for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for v1, v2 being Vector of V st Carrier L = {v1,v2} & v1 <> v2 holds
Sum L = ((L . v1) * v1) + ((L . v2) * v2) by VECTSP_6:21;