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

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