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:111;
reconsider A = {y0,x0} as Subset of (RealVectSpace (Seg n)) ;
A c= Bn

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in A or u in Bn )
assume u in A ; :: thesis: u in Bn
hence u in Bn by A2, A3, TARSKI:def 2; :: thesis: verum

end;

then A5: A is linearly-independent by A1, RLVECT_3:6;
y0 = a * x0 by A4;
hence x = y by A5, RLVECT_3:13; :: thesis: verum