theorem :: RLAFFIN1:84

for r being Real
for V being RealLinearSpace
for v, w, p being VECTOR of V
for I being affinely-independent Subset of V st v in I & w in Affin I & p in Affin (I \ {v}) & w = (r * v) + ((1 - r) * p) holds
r = (w |-- I) . v