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 12;
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