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