theorem Th17: :: RLAFFIN2:17

for V being RealLinearSpace
for F being Subset-Family of V st union F is finite holds
(center_of_mass V) .: F c= conv (union F)