let X be set ; :: thesis: for n being Nat
for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision n,P,KX) = [#] KX
let n be Nat; :: thesis: for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision n,P,KX) = [#] KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function holds [#] (subdivision n,P,KX) = [#] KX
let P be Function; :: thesis: [#] (subdivision n,P,KX) = [#] KX
defpred S₁[ Nat] means [#] (subdivision $1,P,KX) = [#] KX;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
n in NAT by ORDINAL1:def 13;
then A2: subdivision (n + 1),P,KX = subdivision 1,P,(subdivision n,P,KX) by Th63
.= subdivision P,(subdivision n,P,KX) by Th62 ;
assume [#] (subdivision n,P,KX) = [#] KX ; :: thesis: S₁[n + 1]
hence S₁[n + 1] by A2, Def20; :: thesis: verum

end;

A3: S₁[ 0 ] by Th61;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence [#] (subdivision n,P,KX) = [#] KX ; :: thesis: verum