for V being RealLinearSpace
for v1, v2 being VECTOR of V
for a, b being Real st v1 <> v2 holds
ex l being Linear_Combination of {v1,v2} st
( l . v1 = a & l . v2 = b ) by Lm2;