theorem :: CIRCLED1:25

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