theorem Th38: :: SIMPLEX1:38

for V being RealLinearSpace
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & card Sf = card (union Sf) holds
for v being Element of V st not v in union Sf & (union Sf) \/ {v} is affinely-independent holds
{ S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : (center_of_mass V) .: Sf c= S1 } = {(((center_of_mass V) .: Sf) \/ ((center_of_mass V) .: {((union Sf) \/ {v})}))}