let V be RealLinearSpace; :: thesis:
let Kv be non void SimplicialComplex of V; :: thesis:
let S be Simplex of (BCS Kv); :: thesis:
set cM = center_of_mass V;
let F be c=-linear finite finite-membered Subset-Family of V; :: thesis:
assume A1: S = (center_of_mass V) .: F ; :: thesis:
let a1, a2 be VECTOR of V; :: thesis:
assume that
A2: a1 in S and
A3: a2 in S ; :: thesis:
consider A1 being object such that
A4: A1 in dom (center_of_mass V) and
A5: A1 in F and
A6: (center_of_mass V) . A1 = a1 by A1, A2, FUNCT_1:def 6;
consider A2 being object such that
A7: A2 in dom (center_of_mass V) and
A8: A2 in F and
A9: (center_of_mass V) . A2 = a2 by A1, A3, FUNCT_1:def 6;
reconsider A1 = A1, A2 = A2 as set by TARSKI:1;
A10: A1,A2 are_c=-comparable by A5, A8, ORDINAL1:def 8;
set uF = union F;
set CuF = Complex_of {(union F)};
A11: for a1, a2 being VECTOR of V
for A1, A2 being set st A1 c= A2 & A1 in dom (center_of_mass V) & A1 in F & (center_of_mass V) . A1 = a1 & A1 in dom (center_of_mass V) & A2 in F & (center_of_mass V) . A2 = a2 holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )

proof

per cases ;

suppose A31: A1 = A2 ; :: thesis:

reconsider Z = 0 as Real ;
take b1 = a1; :: thesis:
take b2 = a1; :: thesis:
take Z ; :: thesis:
card (union F) >= 1 by A21, NAT_1:14;
then A32: (card (union F)) - 1 >= 1 - 1 by XREAL_1:6;
a1 - a2 = 0. V by A16, A18, A31, RLVECT_1:5;
hence ( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = Z * (b1 - b2) & 0 <= Z & Z <= ((card (union F)) - 1) / (card (union F)) ) by A30, A32, RLVECT_1:10, SIMPLEX0:def 4; :: thesis:

end;

suppose A1 <> A2 ; :: thesis:

then not A2 c= A1 by A13, XBOOLE_0:def 10;
then reconsider A21 = A2 \ A1 as non empty finite Subset of V by XBOOLE_1:37;
A33: A21 in dom (center_of_mass V) by A29, ORDERS_1:2;
then (center_of_mass V) . A21 in rng (center_of_mass V) by FUNCT_1:def 3;
then reconsider a21 = (center_of_mass V) . A21 as VECTOR of V ;
reconsider aa2 = {a21} as Subset of (BCS (Complex_of {(union F)})) by A25, A27, SIMPLEX1:def 5;
A34: a21 in aa2 by TARSKI:def 1;
then reconsider d2 = a21 as Element of (BCS (Complex_of {(union F)})) ;
(center_of_mass V) .: AA2 = Im ((center_of_mass V),A21) by RELAT_1:def 16
.= {a21} by A33, FUNCT_1:59 ;
then aa2 is simplex-like by A24, A26, SIMPLEX0:def 20;
then A35: d2 is vertex-like by A34;
set r1 = 1 / (card A1);
set r2 = 1 / (card A2);
set r21 = 1 / (card A21);
set r = (card A21) / (card A2);
reconsider r1 = 1 / (card A1), r2 = 1 / (card A2), r21 = 1 / (card A21), r = (card A21) / (card A2) as Real ;
take a1 ; :: thesis:
take a21 ; :: thesis:
take r ; :: thesis:
A36: r * r21 = ((card A21) * 1) / ((card A21) * (card A2)) by XCMPLX_1:76
.= r2 by XCMPLX_1:91 ;
consider L1 being Linear_Combination of A1 such that
A37: Sum L1 = r1 * (Sum A1) and
sum L1 = r1 * (card A1) and
A38: L1 = (ZeroLC V) +* (A1 --> r1) by RLAFFIN2:15;
A39: Carrier L1 c= A1 by RLVECT_2:def 6;
A40: card A21 = (1 * (card A2)) - (1 * (card A1)) by A13, CARD_2:44;
then A41: r1 - r2 = ((card A21) * 1) / ((card A2) * (card A1)) by XCMPLX_1:130
.= r * r1 by XCMPLX_1:76 ;
consider L21 being Linear_Combination of A21 such that
A42: Sum L21 = r21 * (Sum A21) and
sum L21 = r21 * (card A21) and
A43: L21 = (ZeroLC V) +* (A21 --> r21) by RLAFFIN2:15;
A44: Carrier L21 c= A21 by RLVECT_2:def 6;
consider L2 being Linear_Combination of A2 such that
A45: Sum L2 = r2 * (Sum A2) and
sum L2 = r2 * (card A2) and
A46: L2 = (ZeroLC V) +* (A2 --> r2) by RLAFFIN2:15;
A47: Carrier L2 c= A2 by RLVECT_2:def 6;
for v being Element of V holds (L1 - L2) . v = (r * (L1 - L21)) . v

proof

let v be Element of V; :: thesis:
A48: dom (A21 --> r21) = A21 by FUNCOP_1:13;
A49: (L1 - L2) . v = (L1 . v) - (L2 . v) by RLVECT_2:54;
A50: dom (A1 --> r1) = A1 by FUNCOP_1:13;
A51: dom (A2 --> r2) = A2 by FUNCOP_1:13;
(r * (L1 - L21)) . v = r * ((L1 - L21) . v) by RLVECT_2:def 11;
then A52: (r * (L1 - L21)) . v = r * ((L1 . v) - (L21 . v)) by RLVECT_2:54;

per cases ;

suppose A53: v in A1 ; :: thesis:

then not v in Carrier L21 by A44, XBOOLE_0:def 5;
then A54: L21 . v = 0 by RLVECT_2:19;
A55: ( (A2 --> r2) . v = r2 & (A1 --> r1) . v = r1 ) by A13, A53, FUNCOP_1:7;
L1 . v = (A1 --> r1) . v by A38, A50, A53, FUNCT_4:13;
hence (L1 - L2) . v = (r * (L1 - L21)) . v by A13, A41, A46, A49, A51, A52, A53, A54, A55, FUNCT_4:13; :: thesis:

end;

suppose A56: ( v in A2 & not v in A1 ) ; :: thesis:

then not v in Carrier L1 by A39;
then A57: L1 . v = 0 by RLVECT_2:19;
(A2 --> r2) . v = r2 by A56, FUNCOP_1:7;
then A58: (L1 - L2) . v = - r2 by A46, A49, A51, A56, A57, FUNCT_4:13;
A59: v in A21 by A56, XBOOLE_0:def 5;
then (A21 --> r21) . v = r21 by FUNCOP_1:7;
then (r * (L1 - L21)) . v = r * (- r21) by A43, A48, A52, A57, A59, FUNCT_4:13;
hence (L1 - L2) . v = (r * (L1 - L21)) . v by A36, A58; :: thesis:

end;

suppose A60: ( not v in A1 & not v in A2 ) ; :: thesis:

then not v in Carrier L1 by A39;
then A61: L1 . v = 0 by RLVECT_2:19;
not v in Carrier L21 by A44, A60, XBOOLE_0:def 5;
then A62: L21 . v = 0 by RLVECT_2:19;
not v in Carrier L2 by A47, A60;
hence (L1 - L2) . v = (r * (L1 - L21)) . v by A49, A52, A62, A61, RLVECT_2:19; :: thesis:

end;

then A63: L1 - L2 = r * (L1 - L21) by RLVECT_2:def 9;
( card A1 >= 1 & card A2 <= card (union F) ) by A17, NAT_1:14, NAT_1:43, ZFMISC_1:74;
then (card A1) * (card (union F)) >= 1 * (card A2) by XREAL_1:66;
then ((card A2) * (card (union F))) - ((card A1) * (card (union F))) <= ((card (union F)) * (card A2)) - (card A2) by XREAL_1:13;
then A64: (card A21) * (card (union F)) <= ((card (union F)) - 1) * (card A2) by A40;
A65: Sum L21 = a21 by A42, RLAFFIN2:def 2;
A66: Sum L1 = a1 by A16, A37, RLAFFIN2:def 2;
Sum L2 = a2 by A18, A45, RLAFFIN2:def 2;
then a1 - a2 = Sum (r * (L1 - L21)) by A63, A66, RLVECT_3:4
.= r * (Sum (L1 - L21)) by RLVECT_3:2
.= r * (a1 - a21) by A65, A66, RLVECT_3:4 ;
hence ( a1 in Vertices (BCS (Complex_of {(union F)})) & a21 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (a1 - a21) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A21, A30, A35, A64, SIMPLEX0:def 4, XREAL_1:102; :: thesis:

end;

per cases by A10, XBOOLE_0:def 9;

suppose A1 c= A2 ; :: thesis:

hence ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A4, A5, A6, A8, A9, A11; :: thesis:

end;

suppose A2 c= A1 ; :: thesis:

then consider b1, b2 being VECTOR of V, r being Real such that
A67: ( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) ) and
A68: a2 - a1 = r * (b1 - b2) and
A69: ( 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A5, A6, A7, A8, A9, A11;
take b2 ; :: thesis:
take b1 ; :: thesis:
take r ; :: thesis:
a1 - a2 = - (r * (b1 - b2)) by A68, RLVECT_1:33
.= r * (- (b1 - b2)) by RLVECT_1:25
.= r * (b2 - b1) by RLVECT_1:33 ;
hence ( b2 in Vertices (BCS (Complex_of {(union F)})) & b1 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b2 - b1) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A67, A69; :: thesis:

end;