let n be Nat; 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; 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; ( |.Kv.| c= [#] Kv implies BCS ((n + 1),Kv) = BCS (BCS (n,Kv)) )
A1:
|.(BCS (n,Kv)).| = |.Kv.|
by Th10;
assume A2:
|.Kv.| c= [#] Kv
; 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; verum