let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function holds subdivision (0,P,KX) = KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function holds subdivision (0,P,KX) = KX
let P be Function; :: thesis: subdivision (0,P,KX) = KX
ex F being Function st
( F . 0 = KX & F . 0 = subdivision (0,P,KX) & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) by Def21;
hence subdivision (0,P,KX) = KX ; :: thesis: verum