let V be RealLinearSpace; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & card Sf = card (union Sf) holds
for v being Element of V st not v in union Sf & (union Sf) \/ {v} is affinely-independent holds
{ S1 where S1 is Simplex of card Sf, BCS (Complex_of {((union Sf) \/ {v})}) : () .: Sf c= S1 } = {((() .: Sf) \/ (() .: {((union Sf) \/ {v})}))}

let S be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( S is with_non-empty_elements & card S = card () implies for v being Element of V st not v in union S & () \/ {v} is affinely-independent holds
{ S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } = {((() .: S) \/ (() .: {(() \/ {v})}))} )

assume that
A1: S is with_non-empty_elements and
A2: card S = card () ; :: thesis: for v being Element of V st not v in union S & () \/ {v} is affinely-independent holds
{ S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } = {((() .: S) \/ (() .: {(() \/ {v})}))}

set U = union S;
set B = center_of_mass V;
let v be Element of V; :: thesis: ( not v in union S & () \/ {v} is affinely-independent implies { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } = {((() .: S) \/ (() .: {(() \/ {v})}))} )
assume that
A3: not v in union S and
A4: (union S) \/ {v} is affinely-independent ; :: thesis: { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } = {((() .: S) \/ (() .: {(() \/ {v})}))}
reconsider Uv = () \/ {v} as finite affinely-independent Subset of V by A4;
set CUv = Complex_of {Uv};
set BC = BCS ();
set SS = { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } ;
set TT = {((() .: S) \/ (() .: {(() \/ {v})}))};
A5: union S c= Uv by XBOOLE_1:7;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {((() .: S) \/ (() .: {(() \/ {v})}))} c= { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 }
let x be object ; :: thesis: ( x in { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } implies x in {((() .: S) \/ (() .: {(() \/ {v})}))} )
reconsider n = 0 as Nat ;
assume x in { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } ; :: thesis: x in {((() .: S) \/ (() .: {(() \/ {v})}))}
then consider S1 being Simplex of card S, BCS () such that
A6: x = S1 and
A7: (center_of_mass V) .: S c= S1 ;
((card S) + n) + 1 <= card Uv by ;
then consider T being finite Subset-Family of V such that
A8: T misses S and
A9: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and
A10: card T = n + 1 and
A11: union T c= Uv and
A12: @ S1 = (() .: S) \/ (() .: T) by A1, A5, A7, Th35;
A13: ex x being object st T = {x} by ;
A14: union (T \/ S) = () \/ () by ZFMISC_1:78;
T \/ S is finite-membered
proof
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in T \/ S or x is finite )
assume x in T \/ S ; :: thesis: x is finite
then x c= union (T \/ S) by ZFMISC_1:74;
hence x is finite by ; :: thesis: verum
end;
then reconsider TS = T \/ S as finite finite-membered Subset-Family of V ;
union (T \/ S) c= Uv by ;
then A15: card (union TS) c= card Uv by CARD_1:11;
card TS = (card S) + 1 by ;
then A16: card TS = card Uv by ;
card TS c= card (union TS) by ;
then card (union TS) = card TS by ;
then A17: union TS = Uv by ;
A18: union S c= union (T \/ S) by ;
A19: not union TS in S
proof end;
not T is empty by A10;
then union TS in TS by ;
then union TS in T by ;
then T = {Uv} by ;
hence x in {((() .: S) \/ (() .: {(() \/ {v})}))} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((() .: S) \/ (() .: {(() \/ {v})}))} or x in { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } )
assume x in {((() .: S) \/ (() .: {(() \/ {v})}))} ; :: thesis: x in { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 }
then A21: x = (() .: S) \/ (() .: {Uv}) by TARSKI:def 1;
( (center_of_mass V) .: S c= (() .: S) \/ (() .: {Uv}) & (() .: S) \/ (() .: {Uv}) is Simplex of card S, BCS () ) by ;
hence x in { S1 where S1 is Simplex of card S, BCS (Complex_of {(() \/ {v})}) : () .: S c= S1 } by A21; :: thesis: verum