for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is circled & Carrier L = {v} holds
( L . v = 1 & Sum L = (L . v) * v )