let n be Nat; :: thesis: 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
let Bn be Subset of (RealVectSpace (Seg n)); :: thesis: 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
let x, y be Element of REAL n; :: thesis: for a being Real st Bn is linearly-independent & x in Bn & y in Bn & y = a * x holds
x = y
let a be Real; :: thesis: ( Bn is linearly-independent & x in Bn & y in Bn & y = a * x implies x = y )
assume that
A1: Bn is linearly-independent and
A2: x in Bn and
A3: y in Bn and
A4: y = a * x ; :: thesis: x = y
reconsider x0 = x, y0 = y as Element of (RealVectSpace (Seg n)) by FINSEQ_2:93;
reconsider A = {y0,x0} as Subset of (RealVectSpace (Seg n)) ;
A c= Bn by A2, A3, TARSKI:def 2;
then A5: A is linearly-independent by A1, RLVECT_3:5;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
y0 = aa * x0 by A4;
hence x = y by A5, RLVECT_3:12; :: thesis: verum