for V being RealLinearSpace
for Af being finite Subset of V
for If being finite affinely-independent Subset of V
for L being Linear_Combination of Af st Af c= conv If & sum L = 1 holds
( Sum L in Affin If & ( for x being Element of V ex F being FinSequence of REAL ex G being FinSequence of V st
( ((Sum L) |-- If) . x = Sum F & len G = len F & G is one-to-one & rng G = Carrier L & ( for n being Nat st n in dom F holds
F . n = (L . (G . n)) * (((G . n) |-- If) . x) ) ) ) )