let V be RealLinearSpace; :: thesis: for Aff being finite affinely-independent Subset of V
for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
let Aff be finite affinely-independent Subset of V; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & union Sf c= Aff holds
( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
let Sf be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( Sf is with_non-empty_elements & union Sf c= Aff implies ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) )
reconsider N = 0 as Nat ;
set U = union Sf;
assume that
A1: Sf is with_non-empty_elements and
A2: union Sf c= Aff ; :: thesis: ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) iff for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) )
set B = center_of_mass V;
set C = Complex_of {Aff};
reconsider s = Sf as c=-linear finite Subset-Family of (Complex_of {Aff}) ;
A3: the topology of (Complex_of {Aff}) = bool Aff by SIMPLEX0:4;
Segm (card (union Sf)) c= Segm (card Aff) by A2, CARD_1:11;
then card (union Sf) <= card Aff by NAT_1:39;
then A4: ( N - 1 <= (card (union Sf)) - 1 & (card (union Sf)) - 1 <= (card Aff) - 1 ) by XREAL_1:9;
( Sf c= bool (union Sf) & bool (union Sf) c= bool Aff ) by A2, ZFMISC_1:67, ZFMISC_1:82;
then A5: s c= the topology of (Complex_of {Aff}) by A3;
A6: s is simplex-like

proof

let a be Subset of (Complex_of {Aff}); :: according to TOPS_2:def 1 :: thesis: ( not a in s or not a is dependent )
assume a in s ; :: thesis: not a is dependent
hence not a is dependent by A5; :: thesis: verum

end;

then A7: card s = card ((center_of_mass V) .: Sf) by A1, Th33;
Segm (card Sf) c= Segm (card (union Sf)) by A1, SIMPLEX0:10;
then A8: card Sf <= card (union Sf) by NAT_1:39;
set BC = BCS (Complex_of {Aff});
reconsider c = card Aff as ExtReal ;
A9: degree (Complex_of {Aff}) = c - 1 by SIMPLEX0:26
.= (card Aff) + (- 1) by XXREAL_3:def 2 ;
A10: |.(Complex_of {Aff}).| c= [#] (Complex_of {Aff}) ;
then A11: BCS (Complex_of {Aff}) = subdivision ((center_of_mass V),(Complex_of {Aff})) by Def5;
then [#] (BCS (Complex_of {Aff})) = [#] (Complex_of {Aff}) by SIMPLEX0:def 20;
then reconsider BS = (center_of_mass V) .: Sf as Subset of (BCS (Complex_of {Aff})) ;
A12: N - 1 <= (card Aff) - 1 by XREAL_1:9;
A13: degree (BCS (Complex_of {Aff})) = degree (Complex_of {Aff}) by A10, Th31;
thus ( (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) implies for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) :: thesis: ( ( for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ) implies (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) )

proof

assume (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) ; :: thesis: for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n )
then reconsider BS = (center_of_mass V) .: Sf as Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) ;
reconsider c1 = (card (union Sf)) - 1 as ExtReal ;
let n be Nat; :: thesis: ( 0 < n & n <= card (union Sf) implies ex x being set st
( x in Sf & card x = n ) )
reconsider s = Sf as Subset-Family of (union Sf) by ZFMISC_1:82;
defpred S₁[ Nat] means ( $1 < card Sf implies ex x being finite set st
( x in Sf & card x = (card Sf) - $1 ) );
assume that
A14: 0 < n and
A15: n <= card (union Sf) ; :: thesis: ex x being set st
( x in Sf & card x = n )
A16: (card Sf) - 0 > (card Sf) - n by A14, XREAL_1:10;
A17: card BS = c1 + 1 by A4, A9, A13, SIMPLEX0:def 18
.= ((card (union Sf)) - 1) + 1 by XXREAL_3:def 2
.= card (union Sf) ;
then A18: not Sf is empty by A14, A15;
then consider s1 being Subset-Family of (union Sf) such that
A19: s c= s1 and
( s1 is with_non-empty_elements & s1 is c=-linear ) and
A20: card (union Sf) = card s1 and
A21: for Z being set st Z in s1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in s1 ) by A1, SIMPLEX0:9, SIMPLEX0:13;
card (union Sf) = card Sf by A1, A6, A17, Th33;
then A22: s = s1 by A19, A20, CARD_2:102;
A23: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A24: S₁[n] ; :: thesis: S₁[n + 1]
assume A25: n + 1 < card Sf ; :: thesis: ex x being finite set st
( x in Sf & card x = (card Sf) - (n + 1) )
then consider X being finite set such that
A26: X in Sf and
A27: card X = (card Sf) - n by A24, NAT_1:13;
A28: (n + 1) - n < (card Sf) - n by A25, XREAL_1:9;
then consider x being set such that
A29: ( x in X & X \ {x} in Sf ) by A21, A22, A26, A27;
reconsider C = (card X) - 1 as Element of NAT by A27, A28, NAT_1:20;
take X \ {x} ; :: thesis: ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) )
card X = C + 1 ;
hence ( X \ {x} in Sf & card (X \ {x}) = (card Sf) - (n + 1) ) by A27, A29, STIRL2_1:55; :: thesis: verum

end;

A30: S₁[ 0 ] by A7, A17, A18, SIMPLEX0:9;
A31: for n being Nat holds S₁[n] from NAT_1:sch 2(A30, A23);
(card Sf) - n is Nat by A7, A15, A17, NAT_1:21;
then ex x being finite set st
( x in Sf & card x = (card Sf) - ((card Sf) - n) ) by A16, A31;
hence ex x being set st
( x in Sf & card x = n ) ; :: thesis: verum

end;

assume A32: for n being Nat st 0 < n & n <= card (union Sf) holds
ex x being set st
( x in Sf & card x = n ) ; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

per cases ( union Sf is empty or not union Sf is empty ) ;

suppose A33: union Sf is empty ; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

reconsider O = - 1 as ExtReal ;
A34: ( O <= degree (BCS (Complex_of {Aff})) & 0 = O + 1 ) by A9, A10, A12, Th31, XXREAL_3:7;
Sf is empty by A1, A33;
then A35: BS is empty ;
thus (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by A33, A34, A35, SIMPLEX0:def 18; :: thesis: verum

end;

suppose A36: not union Sf is empty ; :: thesis: (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff})

reconsider c1 = (card (union Sf)) - 1 as ExtReal ;
consider x being set such that
A37: x in Sf and
card x = card (union Sf) by A32, A36;
defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & card D2 = $1 );
A38: for x being object st x in Seg (card (union Sf)) holds
ex y being object st
( y in Sf & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Seg (card (union Sf)) implies ex y being object st
( y in Sf & S₁[x,y] ) )
assume A39: x in Seg (card (union Sf)) ; :: thesis: ex y being object st
( y in Sf & S₁[x,y] )
reconsider n = x as Nat by A39;
( 0 < n & n <= card (union Sf) ) by A39, FINSEQ_1:1;
then ex x being set st
( x in Sf & card x = n ) by A32;
hence ex y being object st
( y in Sf & S₁[x,y] ) ; :: thesis: verum

end;

consider f being Function of (Seg (card (union Sf))),Sf such that
A40: for x being object st x in Seg (card (union Sf)) holds
S₁[x,f . x] from FUNCT_2:sch 1(A38);

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A41: x1 in dom f and
A42: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
A43: S₁[x2,f . x2] by A40, A42;
S₁[x1,f . x1] by A40, A41;
hence x1 = card (f . x1)
.= x2 by A42, A43 ;
:: thesis: verum

end;

then A44: ( rng f c= Sf & f is one-to-one ) by FUNCT_1:def 4;
dom f = Seg (card (union Sf)) by A37, FUNCT_2:def 1;
then ( Segm (card (Seg (card (union Sf)))) = Segm (card (union Sf)) & Segm (card (Seg (card (union Sf)))) c= Segm (card Sf) ) by A44, CARD_1:10, FINSEQ_1:57;
then card (union Sf) <= card Sf by NAT_1:39;
then A45: card BS = card (union Sf) by A7, A8, XXREAL_0:1;
( BS is Simplex of (BCS (Complex_of {Aff})) & c1 + 1 = ((card (union Sf)) - 1) + 1 ) by A6, A11, SIMPLEX0:def 20, XXREAL_3:def 2;
hence (center_of_mass V) .: Sf is Simplex of (card (union Sf)) - 1, BCS (Complex_of {Aff}) by A4, A9, A13, A45, SIMPLEX0:def 18; :: thesis: verum

end;

end;