theorem Th23: :: CIRCLED1:23

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