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:58, RELAT_1:74;
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 object ; :: 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 2;
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 object ; :: 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 ;
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:112
.= (P | Y) .: ((S /\ (dom P)) /\ Y) by A6, A9, RELAT_1:129
.= (P | Y) .: (S /\ ((dom P) /\ Y)) by XBOOLE_1:16
.= (P | Y) .: (S /\ (dom (P | Y))) by RELAT_1:61
.= (P | Y) .: S by RELAT_1:112 ;
then B is simplex-like by Def20;
hence x in the topology of (subdivision ((P | Y),KX)) ; :: thesis: verum

end;

( P | (dom P) = P & P | Y = (P | Y) | (dom (P | Y)) ) ;
then subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision (P,KX) by A1, Th54, RELAT_1:60;
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