let X, Y be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
let KX be SimplicialComplexStr of X; :: thesis: for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
let P be Function; :: thesis: ( P .: the topology of KX c= Y implies subdivision ((Y |` P),KX) = subdivision (P,KX) )
set PK = subdivision (P,KX);
( P = (rng P) |` P & Y |` ((rng P) |` P) = (Y /\ (rng P)) |` P ) by RELAT_1:96;
then reconsider PY = subdivision ((Y |` P),KX) as SubSimplicialComplex of subdivision (P,KX) by Th56, XBOOLE_1:17;
A1: ( [#] PY = [#] KX & [#] (subdivision (P,KX)) = [#] KX ) by Def20;
assume A2: P .: the topology of KX c= Y ; :: thesis: subdivision ((Y |` P),KX) = subdivision (P,KX)
A3: the topology of (subdivision (P,KX)) c= the topology of PY

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision (P,KX)) or x in the topology of PY )
assume x in the topology of (subdivision (P,KX)) ; :: thesis: x in the topology of PY
then reconsider A = x as Simplex of (subdivision (P,KX)) by PRE_TOPC:def 2;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A4: A = P .: S by Def20;
reconsider A = A as Subset of PY by A1;
S c= the topology of KX

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S or y in the topology of KX )
assume A5: y in S ; :: thesis: y in the topology of KX
reconsider y = y as Subset of KX by A5;
y is simplex-like by A5, TOPS_2:def 1;
hence y in the topology of KX ; :: thesis: verum

end;

then A c= P .: the topology of KX by A4, RELAT_1:123;
then A /\ Y = A by A2, XBOOLE_1:1, XBOOLE_1:28;
then A = (Y |` P) .: S by A4, FUNCT_1:67;
then A is simplex-like by Def20;
hence x in the topology of PY ; :: thesis: verum

end;

the topology of PY c= the topology of (subdivision (P,KX)) by Def13;
hence subdivision ((Y |` P),KX) = subdivision (P,KX) by A1, A3, XBOOLE_0:def 10; :: thesis: verum