let V be RealLinearSpace; :: thesis: for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V

for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds

card S = card ((center_of_mass V) .: S)

let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds

card S = card ((center_of_mass V) .: S)

set B = center_of_mass V;

set T = the topology of Kas;

let S be simplex-like Subset-Family of Kas; :: thesis: ( S is with_non-empty_elements implies card S = card ((center_of_mass V) .: S) )

assume A1: S is with_non-empty_elements ; :: thesis: card S = card ((center_of_mass V) .: S)

A2: not {} in S by A1;

[#] Kas c= the carrier of V by SIMPLEX0:def 9;

then bool the carrier of Kas c= bool the carrier of V by ZFMISC_1:67;

then ( dom (center_of_mass V) = (bool the carrier of V) \ {{}} & S c= bool the carrier of V ) by FUNCT_2:def 1;

then A3: dom ((center_of_mass V) | S) = S by A2, RELAT_1:62, ZFMISC_1:34;

S c= the topology of Kas

then A4: (center_of_mass V) | S is one-to-one by FUNCT_1:52;

(center_of_mass V) .: S = rng ((center_of_mass V) | S) by RELAT_1:115;

then S,(center_of_mass V) .: S are_equipotent by A3, A4, WELLORD2:def 4;

hence card S = card ((center_of_mass V) .: S) by CARD_1:5; :: thesis: verum

for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds

card S = card ((center_of_mass V) .: S)

let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds

card S = card ((center_of_mass V) .: S)

set B = center_of_mass V;

set T = the topology of Kas;

let S be simplex-like Subset-Family of Kas; :: thesis: ( S is with_non-empty_elements implies card S = card ((center_of_mass V) .: S) )

assume A1: S is with_non-empty_elements ; :: thesis: card S = card ((center_of_mass V) .: S)

A2: not {} in S by A1;

[#] Kas c= the carrier of V by SIMPLEX0:def 9;

then bool the carrier of Kas c= bool the carrier of V by ZFMISC_1:67;

then ( dom (center_of_mass V) = (bool the carrier of V) \ {{}} & S c= bool the carrier of V ) by FUNCT_2:def 1;

then A3: dom ((center_of_mass V) | S) = S by A2, RELAT_1:62, ZFMISC_1:34;

S c= the topology of Kas

proof

then
((center_of_mass V) | the topology of Kas) | S = (center_of_mass V) | S
by RELAT_1:74;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in the topology of Kas )

assume x in S ; :: thesis: x in the topology of Kas

then x is Simplex of Kas by TOPS_2:def 1;

hence x in the topology of Kas by PRE_TOPC:def 2; :: thesis: verum

end;assume x in S ; :: thesis: x in the topology of Kas

then x is Simplex of Kas by TOPS_2:def 1;

hence x in the topology of Kas by PRE_TOPC:def 2; :: thesis: verum

then A4: (center_of_mass V) | S is one-to-one by FUNCT_1:52;

(center_of_mass V) .: S = rng ((center_of_mass V) | S) by RELAT_1:115;

then S,(center_of_mass V) .: S are_equipotent by A3, A4, WELLORD2:def 4;

hence card S = card ((center_of_mass V) .: S) by CARD_1:5; :: thesis: verum