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

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

(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

sum L = 1
by A2, XCMPLX_1:87;
let v be VECTOR of V; :: thesis: 0 <= L . v

end;per cases
( v in Af or not v in Af )
;

end;

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;.= 1 / (card a) by A6, FUNCOP_1:7 ;

hence 0 <= L . v ; :: thesis: verum

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;.= 0 by RLVECT_2:20 ;

hence 0 <= L . v ; :: thesis: verum

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