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

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