for V being RealLinearSpace
for u, v, w being VECTOR of V
for l being Linear_Combination of {u,v,w} st u <> v & u <> w & v <> w holds
Sum l = (((l . u) * u) + ((l . v) * v)) + ((l . w) * w)