theorem Th39: :: EUCLID_7:40

for n being Nat
for Bn being Subset of (RealVectSpace (Seg n))
for x, y being Element of REAL n
for a being Real st Bn is linearly-independent & x in Bn & y in Bn & y = a * x holds
x = y