let X, Y be set ; 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; for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
let P be Function; ( 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
; subdivision ((Y |` P),KX) = subdivision (P,KX)
A3:
the topology of (subdivision (P,KX)) c= the topology of PY
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; verum