theorem Th15: :: CONVEX4:15

for V being ComplexLinearSpace
for v1, v2 being VECTOR of V st v1 <> v2 holds
for l being C_Linear_Combination of {v1,v2} holds Sum l = ((l . v1) * v1) + ((l . v2) * v2)