let X, Y be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision (P | Y),KX = subdivision P,KX
let KX be SimplicialComplexStr of X; :: thesis: for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision (P | Y),KX = subdivision P,KX
let P be Function; :: thesis: ( (dom P) /\ the topology of KX c= Y implies subdivision (P | Y),KX = subdivision P,KX )
set PX = subdivision (P | Y),KX;
set PP = subdivision P,KX;
A1: (P | Y) | (dom (P | Y)) = P | (dom (P | Y)) by RELAT_1:87, RELAT_1:103;
A2: ( [#] (subdivision (P | Y),KX) = [#] KX & [#] (subdivision P,KX) = [#] KX ) by Def20;
assume A3: (dom P) /\ the topology of KX c= Y ; :: thesis: subdivision (P | Y),KX = subdivision P,KX
A4: the topology of (subdivision P,KX) c= the topology of (subdivision (P | Y),KX)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (subdivision P,KX) or x in the topology of (subdivision (P | Y),KX) )
assume x in the topology of (subdivision P,KX) ; :: thesis: x in the topology of (subdivision (P | Y),KX)
then reconsider A = x as Simplex of (subdivision P,KX) by PRE_TOPC:def 5;
reconsider B = A as Subset of (subdivision (P | Y),KX) by A2;
consider S being c=-linear finite simplex-like Subset-Family of KX such that
A5: A = P .: S by Def20;
A6: S /\ (dom P) c= Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in S /\ (dom P) or x in Y )
assume A7: x in S /\ (dom P) ; :: thesis: x in Y
then reconsider A = x as Subset of KX ;
x in S by A7, XBOOLE_0:def 4;
then A is simplex-like by TOPS_2:def 1;
then A8: A in the topology of KX by PRE_TOPC:def 5;
x in dom P by A7, XBOOLE_0:def 4;
then A in the topology of KX /\ (dom P) by A8, XBOOLE_0:def 4;
hence x in Y by A3; :: thesis: verum

end;

then A9: (S /\ (dom P)) /\ Y = S /\ (dom P) by XBOOLE_1:28;
B = P .: (S /\ (dom P)) by A5, RELAT_1:145
.= (P | Y) .: ((S /\ (dom P)) /\ Y) by A6, A9, RELAT_1:162
.= (P | Y) .: (S /\ ((dom P) /\ Y)) by XBOOLE_1:16
.= (P | Y) .: (S /\ (dom (P | Y))) by RELAT_1:90
.= (P | Y) .: S by RELAT_1:145 ;
then B is simplex-like by Def20;
hence x in the topology of (subdivision (P | Y),KX) by PRE_TOPC:def 5; :: thesis: verum

end;

( P | (dom P) = P & P | Y = (P | Y) | (dom (P | Y)) ) by RELAT_1:98;
then subdivision (P | Y),KX is SubSimplicialComplex of subdivision P,KX by A1, Th54, RELAT_1:89;
then the topology of (subdivision (P | Y),KX) c= the topology of (subdivision P,KX) by Def13;
hence subdivision (P | Y),KX = subdivision P,KX by A2, A4, XBOOLE_0:def 10; :: thesis: verum