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