let n be Nat; :: thesis: for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n)
for v being Element of (REAL-NS n)
for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds
v |-- Ar = w |-- At
let Ar be Subset of (REAL-NS n); :: thesis: for At being Subset of (TOP-REAL n)
for v being Element of (REAL-NS n)
for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds
v |-- Ar = w |-- At
let At be Subset of (TOP-REAL n); :: thesis: for v being Element of (REAL-NS n)
for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds
v |-- Ar = w |-- At
let v be Element of (REAL-NS n); :: thesis: for w being Element of (TOP-REAL n) st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent holds
v |-- Ar = w |-- At
let w be Element of (TOP-REAL n); :: thesis: ( Ar = At & v = w & v in Affin Ar & Ar is affinely-independent implies v |-- Ar = w |-- At )
assume A1: ( Ar = At & v = w & v in Affin Ar & Ar is affinely-independent ) ; :: thesis: v |-- Ar = w |-- At
then A2: At is affinely-independent by Th41;
reconsider h = v |-- Ar as Linear_Combination of At by A1, Th25;
A3: Sum h = Sum (v |-- Ar) by Th23
.= w by A1, RLAFFIN1:def 7 ;
A4: sum h = sum (v |-- Ar) by Th44
.= 1 by RLAFFIN1:def 7, A1 ;
w in Affin At by A1, Th43;
hence v |-- Ar = w |-- At by A2, A3, A4, RLAFFIN1:def 7; :: thesis: verum