let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

BCS (1,Kv) = BCS Kv

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv implies BCS (1,Kv) = BCS Kv )

assume A1: |.Kv.| c= [#] Kv ; :: thesis: BCS (1,Kv) = BCS Kv

hence BCS (1,Kv) = subdivision (1,(center_of_mass V),Kv) by Def6

.= subdivision ((center_of_mass V),Kv) by SIMPLEX0:62

.= BCS Kv by A1, Def5 ;

:: thesis: verum

BCS (1,Kv) = BCS Kv

let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv implies BCS (1,Kv) = BCS Kv )

assume A1: |.Kv.| c= [#] Kv ; :: thesis: BCS (1,Kv) = BCS Kv

hence BCS (1,Kv) = subdivision (1,(center_of_mass V),Kv) by Def6

.= subdivision ((center_of_mass V),Kv) by SIMPLEX0:62

.= BCS Kv by A1, Def5 ;

:: thesis: verum