let n be Nat; :: thesis: for V being RealLinearSpace

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

[#] (BCS (n,Kv)) = [#] Kv

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

[#] (BCS (n,Kv)) = [#] Kv

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

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

then BCS (n,Kv) = subdivision (n,(center_of_mass V),Kv) by Def6;

hence [#] (BCS (n,Kv)) = [#] Kv by SIMPLEX0:64; :: thesis: verum

for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds

[#] (BCS (n,Kv)) = [#] Kv

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

[#] (BCS (n,Kv)) = [#] Kv

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

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

then BCS (n,Kv) = subdivision (n,(center_of_mass V),Kv) by Def6;

hence [#] (BCS (n,Kv)) = [#] Kv by SIMPLEX0:64; :: thesis: verum