let V be RealLinearSpace; :: thesis: for Af being finite Subset of V st not Af is empty holds
(center_of_mass V) . Af in conv Af
let Af be finite Subset of V; :: thesis: ( not Af is empty implies (center_of_mass V) . Af in conv Af )
assume not Af is empty ; :: thesis: (center_of_mass V) . Af in conv Af
then reconsider a = Af as non empty finite Subset of V ;
consider L being Linear_Combination of Af such that
A1: Sum L = (1 / (card a)) * (Sum a) and
A2: sum L = (1 / (card a)) * (card a) and
A3: L = (ZeroLC V) +* (Af --> (1 / (card a))) by Th15;
A4: dom (Af --> (1 / (card a))) = Af ;
A5: for v being VECTOR of V holds 0 <= L . v
proof
let v be VECTOR of V; :: thesis: 0 <= L . v
per cases ( v in Af or not v in Af ) ;
suppose A6: v in Af ; :: thesis: 0 <= L . v
then L . v = (Af --> (1 / (card a))) . v by A3, A4, FUNCT_4:13
.= 1 / (card a) by A6, FUNCOP_1:7 ;
hence 0 <= L . v ; :: thesis: verum
end;
suppose not v in Af ; :: thesis: 0 <= L . v
then L . v = (ZeroLC V) . v by A3, A4, FUNCT_4:11
.= 0 by RLVECT_2:20 ;
hence 0 <= L . v ; :: thesis: verum
end;
end;
end;
sum L = 1 by A2, XCMPLX_1:87;
then A7: L is convex by A5, RLAFFIN1:62;
then L in ConvexComb V by CONVEX3:def 1;
then Sum L in { (Sum K) where K is Convex_Combination of a : K in ConvexComb V } by A7;
then Sum L in conv Af by CONVEX3:5;
hence (center_of_mass V) . Af in conv Af by A1, Def2; :: thesis: verum