let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let KX be SimplicialComplexStr of X; :: thesis: for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let SX be SubSimplicialComplex of KX; :: thesis: for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
let P be Function; :: thesis: for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
set PK = subdivision (P,KX);
reconsider PS = subdivision (P,SX) as strict SubSimplicialComplex of subdivision (P,KX) by Th58;
let A be Subset of (subdivision (P,KX)); :: thesis: ( dom P c= the topology of SX & A = [#] SX implies subdivision (P,SX) = (subdivision (P,KX)) | A )
assume that
A1: dom P c= the topology of SX and
A2: A = [#] SX ; :: thesis: subdivision (P,SX) = (subdivision (P,KX)) | A

now

let a be Subset of PS; :: thesis: ( a in the topology of (subdivision (P,KX)) implies a is simplex-like )
assume a in the topology of (subdivision (P,KX)) ; :: thesis: a is simplex-like
then reconsider b = a as Simplex of (subdivision (P,KX)) by PRE_TOPC:def 2;
consider SS being c=-linear finite simplex-like Subset-Family of KX such that
A3: b = P .: SS by Def20;
SS /\ (dom P) c= dom P by XBOOLE_1:17;
then A4: SS /\ (dom P) c= the topology of SX by A1, XBOOLE_1:1;
SS /\ (dom P) c= SS by XBOOLE_1:17;
then reconsider Sd = SS /\ (dom P) as c=-linear finite Subset-Family of SX by A4, XBOOLE_1:1;
A5: Sd is simplex-like

proof

let B be Subset of SX; :: according to TOPS_2:def 1 :: thesis: ( not B in Sd or B is simplex-like )
assume B in Sd ; :: thesis: B is simplex-like
then B in dom P by XBOOLE_0:def 4;
hence B is simplex-like by A1, PRE_TOPC:def 2; :: thesis: verum

end;

P .: SS = P .: Sd by RELAT_1:112;
hence a is simplex-like by A3, A5, Def20; :: thesis: verum

end;

then A6: PS is maximal by Def14;
[#] PS = [#] SX by Def20;
hence subdivision (P,SX) = (subdivision (P,KX)) | A by A2, A6, Def16; :: thesis: verum