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