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

for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds

(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

let v be VECTOR of V; :: thesis: for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds

(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

let Af be finite Subset of V; :: thesis: ( v in Af & not Af \ {v} is empty implies (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) )

set Av = Af \ {v};

assume that

A1: v in Af and

A2: not Af \ {v} is empty ; :: thesis: (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

consider L3 being Linear_Combination of {v} such that

A3: L3 . v = jj / (card Af) by RLVECT_4:37;

consider L1 being Linear_Combination of Af \ {v} such that

A4: Sum L1 = (1 / (card (Af \ {v}))) * (Sum (Af \ {v})) and

sum L1 = (1 / (card (Af \ {v}))) * (card (Af \ {v})) and

A5: L1 = (ZeroLC V) +* ((Af \ {v}) --> (1 / (card (Af \ {v})))) by Th15;

consider L2 being Linear_Combination of Af such that

A6: Sum L2 = (1 / (card Af)) * (Sum Af) and

sum L2 = (1 / (card Af)) * (card Af) and

A7: L2 = (ZeroLC V) +* (Af --> (1 / (card Af))) by Th15;

A8: Sum L1 = (center_of_mass V) . (Af \ {v}) by A2, A4, Def2;

for u being Element of V holds L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u

dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;

then A25: Af \ {v} in dom (center_of_mass V) by A2, ZFMISC_1:56;

Sum L2 = (center_of_mass V) . Af by A1, A6, Def2;

hence (center_of_mass V) . Af = (Sum ((1 - (1 / (card Af))) * L1)) + (Sum L3) by A24, RLVECT_3:1

.= ((1 - (1 / (card Af))) * (Sum L1)) + (Sum L3) by RLVECT_3:2

.= ((1 - (1 / (card Af))) * (Sum L1)) + ((1 / (card Af)) * v) by A3, RLVECT_2:32

.= ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) by A8, A25, PARTFUN1:def 6 ;

:: thesis: verum

for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds

(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

let v be VECTOR of V; :: thesis: for Af being finite Subset of V st v in Af & not Af \ {v} is empty holds

(center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

let Af be finite Subset of V; :: thesis: ( v in Af & not Af \ {v} is empty implies (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) )

set Av = Af \ {v};

assume that

A1: v in Af and

A2: not Af \ {v} is empty ; :: thesis: (center_of_mass V) . Af = ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v)

consider L3 being Linear_Combination of {v} such that

A3: L3 . v = jj / (card Af) by RLVECT_4:37;

consider L1 being Linear_Combination of Af \ {v} such that

A4: Sum L1 = (1 / (card (Af \ {v}))) * (Sum (Af \ {v})) and

sum L1 = (1 / (card (Af \ {v}))) * (card (Af \ {v})) and

A5: L1 = (ZeroLC V) +* ((Af \ {v}) --> (1 / (card (Af \ {v})))) by Th15;

consider L2 being Linear_Combination of Af such that

A6: Sum L2 = (1 / (card Af)) * (Sum Af) and

sum L2 = (1 / (card Af)) * (card Af) and

A7: L2 = (ZeroLC V) +* (Af --> (1 / (card Af))) by Th15;

A8: Sum L1 = (center_of_mass V) . (Af \ {v}) by A2, A4, Def2;

for u being Element of V holds L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u

proof

then A24:
L2 = ((1 - (1 / (card Af))) * L1) + L3
;
let u be Element of V; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u

A9: ( (((1 - (1 / (card Af))) * L1) + L3) . u = (((1 - (1 / (card Af))) * L1) . u) + (L3 . u) & ((1 - (1 / (card Af))) * L1) . u = (1 - (1 / (card Af))) * (L1 . u) ) by RLVECT_2:def 10, RLVECT_2:def 11;

A10: (ZeroLC V) . u = 0 by RLVECT_2:20;

A11: Carrier L3 c= {v} by RLVECT_2:def 6;

A12: dom (Af --> (1 / (card Af))) = Af ;

A13: dom ((Af \ {v}) --> (1 / (card (Af \ {v})))) = Af \ {v} ;

end;A9: ( (((1 - (1 / (card Af))) * L1) + L3) . u = (((1 - (1 / (card Af))) * L1) . u) + (L3 . u) & ((1 - (1 / (card Af))) * L1) . u = (1 - (1 / (card Af))) * (L1 . u) ) by RLVECT_2:def 10, RLVECT_2:def 11;

A10: (ZeroLC V) . u = 0 by RLVECT_2:20;

A11: Carrier L3 c= {v} by RLVECT_2:def 6;

A12: dom (Af --> (1 / (card Af))) = Af ;

A13: dom ((Af \ {v}) --> (1 / (card (Af \ {v})))) = Af \ {v} ;

per cases
( not u in Af or v = u or ( u in Af & u <> v ) )
;

end;

suppose A14:
not u in Af
; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u

then
not u in Carrier L3
by A1, A11, TARSKI:def 1;

then A15: L3 . u = 0 ;

not u in Af \ {v} by A14, ZFMISC_1:56;

then L1 . u = 0 by A5, A10, A13, FUNCT_4:11;

hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A7, A9, A10, A12, A14, A15, FUNCT_4:11; :: thesis: verum

end;then A15: L3 . u = 0 ;

not u in Af \ {v} by A14, ZFMISC_1:56;

then L1 . u = 0 by A5, A10, A13, FUNCT_4:11;

hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A7, A9, A10, A12, A14, A15, FUNCT_4:11; :: thesis: verum

suppose A16:
v = u
; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u

then
not u in Af \ {v}
by ZFMISC_1:56;

then A17: L1 . u = 0 by A5, A10, A13, FUNCT_4:11;

L2 . u = (Af --> (1 / (card Af))) . v by A1, A7, A12, A16, FUNCT_4:13;

hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A1, A3, A9, A16, A17, FUNCOP_1:7; :: thesis: verum

end;then A17: L1 . u = 0 by A5, A10, A13, FUNCT_4:11;

L2 . u = (Af --> (1 / (card Af))) . v by A1, A7, A12, A16, FUNCT_4:13;

hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A1, A3, A9, A16, A17, FUNCOP_1:7; :: thesis: verum

suppose A18:
( u in Af & u <> v )
; :: thesis: L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u

then
L2 . u = (Af --> (1 / (card Af))) . u
by A7, A12, FUNCT_4:13;

then A19: L2 . u = 1 / (card Af) by A18, FUNCOP_1:7;

not u in Carrier L3 by A11, A18, TARSKI:def 1;

then A20: L3 . u = 0 ;

( not v in Af \ {v} & (Af \ {v}) \/ {v} = Af ) by A1, ZFMISC_1:56, ZFMISC_1:116;

then A21: card Af = (card (Af \ {v})) + 1 by CARD_2:41;

1 - (1 / (card Af)) = ((card Af) / (card Af)) - (1 / (card Af)) by A1, XCMPLX_1:60

.= ((card Af) - 1) / (card Af) by XCMPLX_1:120

.= (card (Af \ {v})) / (card Af) by A21 ;

then A22: (1 - (1 / (card Af))) * (1 / (card (Af \ {v}))) = ((card (Af \ {v})) / (card Af)) / (card (Af \ {v})) by XCMPLX_1:99

.= ((card (Af \ {v})) / (card (Af \ {v}))) / (card Af) by XCMPLX_1:48

.= 1 / (card Af) by A2, XCMPLX_1:60 ;

A23: u in Af \ {v} by A18, ZFMISC_1:56;

then L1 . u = ((Af \ {v}) --> (1 / (card (Af \ {v})))) . u by A5, A13, FUNCT_4:13;

hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A9, A19, A20, A22, A23, FUNCOP_1:7; :: thesis: verum

end;then A19: L2 . u = 1 / (card Af) by A18, FUNCOP_1:7;

not u in Carrier L3 by A11, A18, TARSKI:def 1;

then A20: L3 . u = 0 ;

( not v in Af \ {v} & (Af \ {v}) \/ {v} = Af ) by A1, ZFMISC_1:56, ZFMISC_1:116;

then A21: card Af = (card (Af \ {v})) + 1 by CARD_2:41;

1 - (1 / (card Af)) = ((card Af) / (card Af)) - (1 / (card Af)) by A1, XCMPLX_1:60

.= ((card Af) - 1) / (card Af) by XCMPLX_1:120

.= (card (Af \ {v})) / (card Af) by A21 ;

then A22: (1 - (1 / (card Af))) * (1 / (card (Af \ {v}))) = ((card (Af \ {v})) / (card Af)) / (card (Af \ {v})) by XCMPLX_1:99

.= ((card (Af \ {v})) / (card (Af \ {v}))) / (card Af) by XCMPLX_1:48

.= 1 / (card Af) by A2, XCMPLX_1:60 ;

A23: u in Af \ {v} by A18, ZFMISC_1:56;

then L1 . u = ((Af \ {v}) --> (1 / (card (Af \ {v})))) . u by A5, A13, FUNCT_4:13;

hence L2 . u = (((1 - (1 / (card Af))) * L1) + L3) . u by A9, A19, A20, A22, A23, FUNCOP_1:7; :: thesis: verum

dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def 1;

then A25: Af \ {v} in dom (center_of_mass V) by A2, ZFMISC_1:56;

Sum L2 = (center_of_mass V) . Af by A1, A6, Def2;

hence (center_of_mass V) . Af = (Sum ((1 - (1 / (card Af))) * L1)) + (Sum L3) by A24, RLVECT_3:1

.= ((1 - (1 / (card Af))) * (Sum L1)) + (Sum L3) by RLVECT_3:2

.= ((1 - (1 / (card Af))) * (Sum L1)) + ((1 / (card Af)) * v) by A3, RLVECT_2:32

.= ((1 - (1 / (card Af))) * ((center_of_mass V) /. (Af \ {v}))) + ((1 / (card Af)) * v) by A8, A25, PARTFUN1:def 6 ;

:: thesis: verum