for X being set
for KX being SimplicialComplexStr of X
for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))