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