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 12;
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