let X be set ; for n being Nat
for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
let n be Nat; for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
let KX be SimplicialComplexStr of X; for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
let P be Function; [#] (subdivision (n,P,KX)) = [#] KX
defpred S1[ Nat] means [#] (subdivision ($1,P,KX)) = [#] KX;
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[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
;
S1[n + 1]
hence
S1[
n + 1]
by A2, Def20;
verum
end;
A3:
S1[ 0 ]
by Th61;
for n being Nat holds S1[n]
from NAT_1:sch 2(A3, A1);
hence
[#] (subdivision (n,P,KX)) = [#] KX
; verum