theorem Th46: :: SIMPLEX1:46

for k being Nat
for V being RealLinearSpace
for Aff being finite affinely-independent Subset of V
for F being Function of (Vertices (BCS (k,(Complex_of {Aff})))),Aff st ( for v being Vertex of (BCS (k,(Complex_of {Aff})))
for B being Subset of V st B c= Aff & v in conv B holds
F . v in B ) holds
ex n being Nat st card { S where S is Simplex of (card Aff) - 1, BCS (k,(Complex_of {Aff})) : F .: S = Aff } = (2 * n) + 1