let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function holds subdivision 1,P,KX = subdivision P,KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function holds subdivision 1,P,KX = subdivision P,KX
let P be Function; :: thesis: subdivision 1,P,KX = subdivision P,KX
consider F being Function such that
A1: F . 0 = KX and
A2: F . 1 = subdivision 1,P,KX and
dom F = NAT and
A3: for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision P,KX1 by Def21;
F . (0 + 1) = subdivision P,KX by A1, A3;
hence subdivision 1,P,KX = subdivision P,KX by A2; :: thesis: verum