theorem :: CONVEX1:29

for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds
( ((L . v1) + (L . v2)) + (L . v3) = 1 & L . v1 >= 0 & L . v2 >= 0 & L . v3 >= 0 & Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) by Lm15;