let n be Nat; :: thesis: for V being RealLinearSpace
for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS (n + 1),Kv = BCS (BCS n,Kv)
let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv holds
BCS (n + 1),Kv = BCS (BCS n,Kv)
let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv implies BCS (n + 1),Kv = BCS (BCS n,Kv) )
A1: |.(BCS n,Kv).| = |.Kv.| by Th10;
assume A2: |.Kv.| c= [#] Kv ; :: thesis: BCS (n + 1),Kv = BCS (BCS n,Kv)
then A3: [#] (BCS n,Kv) = [#] Kv by Th18;
n in NAT by ORDINAL1:def 13;
then subdivision (1 + n),(center_of_mass V),Kv = subdivision 1,(center_of_mass V),(subdivision n,(center_of_mass V),Kv) by SIMPLEX0:63
.= subdivision 1,(center_of_mass V),(BCS n,Kv) by A2, Def6
.= BCS 1,(BCS n,Kv) by A2, A3, A1, Def6
.= BCS (BCS n,Kv) by A2, A3, A1, Th17 ;
hence BCS (n + 1),Kv = BCS (BCS n,Kv) by A2, Def6; :: thesis: verum