theorem :: RLVECT_4:39

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