theorem Th61: :: SIMPLEX0:61

for X being set
for KX being SimplicialComplexStr of X
for P being Function holds subdivision (0,P,KX) = KX