let x be set ; :: thesis: for V being RealLinearSpace
for B being Subset of V
for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
let V be RealLinearSpace; :: thesis: for B being Subset of V
for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
let B be Subset of V; :: thesis: for I being affinely-independent Subset of V st B c= I & x in Affin B holds
x |-- B = x |-- I
let I be affinely-independent Subset of V; :: thesis: ( B c= I & x in Affin B implies x |-- B = x |-- I )
assume that
A1: B c= I and
A2: x in Affin B ; :: thesis: x |-- B = x |-- I
B is affinely-independent by A1, Th43;
then A3: ( Sum (x |-- B) = x & sum (x |-- B) = 1 ) by A2, Def7;
( Affin B c= Affin I & x |-- B is Linear_Combination of I ) by A1, Th52, RLVECT_2:21;
hence x |-- B = x |-- I by A2, A3, Def7; :: thesis: verum