theorem :: RLVECT_3:13

for V being RealLinearSpace
for v1, v2 being VECTOR of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )