for V being RealLinearSpace
for v being VECTOR of V
for a being Real ex l being Linear_Combination of {v} st l . v = a by Lm1;