for V being RealLinearSpace
for u, v being VECTOR of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds
( a = 0 & b = 0 ) ) holds
( u <> v & u <> 0. V & v <> 0. V )