let X be set ; :: thesis: for n being Nat
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let n be Nat; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let SX be SubSimplicialComplex of KX; :: thesis: for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
let P be Function; :: thesis: subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
defpred S₁[ Nat] means subdivision ($1,P,SX) is SubSimplicialComplex of subdivision ($1,P,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] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider Pn = subdivision (n,P,SX) as SubSimplicialComplex of subdivision (n,P,KX) ;
A2: n in NAT by ORDINAL1:def 12;
then A3: subdivision ((n + 1),P,SX) = subdivision (1,P,Pn) by Th63
.= subdivision (P,Pn) by Th62 ;
subdivision ((n + 1),P,KX) = subdivision (1,P,(subdivision (n,P,KX))) by A2, Th63
.= subdivision (P,(subdivision (n,P,KX))) by Th62 ;
hence S₁[n + 1] by A3, Th58; :: thesis: verum

end;

subdivision (0,P,SX) = SX by Th61;
then A4: S₁[ 0 ] by Th61;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX) ; :: thesis: verum