let X be set ; for KX being SimplicialComplexStr of X
for P being Function holds subdivision (0,P,KX) = KX
let KX be SimplicialComplexStr of X; for P being Function holds subdivision (0,P,KX) = KX
let P be Function; 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
; verum