theorem Th22: :: RLAFFIN2:22

for V being RealLinearSpace
for v being VECTOR of V
for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds
(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)