let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for If being finite affinely-independent Subset of V st v in If holds

(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

let v be VECTOR of V; :: thesis: for If being finite affinely-independent Subset of V st v in If holds

(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

let If be finite affinely-independent Subset of V; :: thesis: ( v in If implies (((center_of_mass V) . If) |-- If) . v = 1 / (card If) )

consider L being Linear_Combination of If such that

A1: ( Sum L = (1 / (card If)) * (Sum If) & sum L = (1 / (card If)) * (card If) ) and

A2: L = (ZeroLC V) +* (If --> (1 / (card If))) by Th15;

assume A3: v in If ; :: thesis: (((center_of_mass V) . If) |-- If) . v = 1 / (card If)

then A4: ( conv If c= Affin If & (center_of_mass V) . If in conv If ) by Th16, RLAFFIN1:65;

( (center_of_mass V) . If = Sum L & sum L = 1 ) by A1, A3, Def2, XCMPLX_1:87;

then ( dom (If --> (1 / (card If))) = If & L = ((center_of_mass V) . If) |-- If ) by A4, RLAFFIN1:def 7;

hence (((center_of_mass V) . If) |-- If) . v = (If --> (1 / (card If))) . v by A2, A3, FUNCT_4:13

.= 1 / (card If) by A3, FUNCOP_1:7 ;

:: thesis: verum

for If being finite affinely-independent Subset of V st v in If holds

(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

let v be VECTOR of V; :: thesis: for If being finite affinely-independent Subset of V st v in If holds

(((center_of_mass V) . If) |-- If) . v = 1 / (card If)

let If be finite affinely-independent Subset of V; :: thesis: ( v in If implies (((center_of_mass V) . If) |-- If) . v = 1 / (card If) )

consider L being Linear_Combination of If such that

A1: ( Sum L = (1 / (card If)) * (Sum If) & sum L = (1 / (card If)) * (card If) ) and

A2: L = (ZeroLC V) +* (If --> (1 / (card If))) by Th15;

assume A3: v in If ; :: thesis: (((center_of_mass V) . If) |-- If) . v = 1 / (card If)

then A4: ( conv If c= Affin If & (center_of_mass V) . If in conv If ) by Th16, RLAFFIN1:65;

( (center_of_mass V) . If = Sum L & sum L = 1 ) by A1, A3, Def2, XCMPLX_1:87;

then ( dom (If --> (1 / (card If))) = If & L = ((center_of_mass V) . If) |-- If ) by A4, RLAFFIN1:def 7;

hence (((center_of_mass V) . If) |-- If) . v = (If --> (1 / (card If))) . v by A2, A3, FUNCT_4:13

.= 1 / (card If) by A3, FUNCOP_1:7 ;

:: thesis: verum