:: deftheorem Def2 defines center_of_mass RLAFFIN2:def 2 :
for V being RealLinearSpace
for b₂ being Function of (BOOL the carrier of V), the carrier of V holds
( b₂ = center_of_mass V iff ( ( for A being non empty finite Subset of V holds b₂ . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds
b₂ . A = 0. V ) ) );