theorem Th7: :: RLVECT_4:7

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