let X be non empty TopSpace; :: thesis: for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 = A holds
for x0 being Point of X0 holds (modid X,A) | X0 is_continuous_at x0
let A be Subset of X; :: thesis: for X0 being non empty SubSpace of X st the carrier of X0 = A holds
for x0 being Point of X0 holds (modid X,A) | X0 is_continuous_at x0
let X0 be non empty SubSpace of X; :: thesis: ( the carrier of X0 = A implies for x0 being Point of X0 holds (modid X,A) | X0 is_continuous_at x0 )
assume A1: the carrier of X0 = A ; :: thesis: for x0 being Point of X0 holds (modid X,A) | X0 is_continuous_at x0
let x0 be Point of X0; :: thesis: (modid X,A) | X0 is_continuous_at x0

now

let W be Subset of (X modified_with_respect_to A); :: thesis: ( W is open & ((modid X,A) | X0) . x0 in W implies ex V being Subset of X0 st
( V is open & x0 in V & ((modid X,A) | X0) .: V c= W ) )
assume A2: ( W is open & ((modid X,A) | X0) . x0 in W ) ; :: thesis: ex V being Subset of X0 st
( V is open & x0 in V & ((modid X,A) | X0) .: V c= W )
then W in A -extension_of_the_topology_of X by PRE_TOPC:def 5;
then consider H, G being Subset of X such that
A3: W = H \/ (G /\ A) and
A4: ( H in the topology of X & G in the topology of X ) ;
reconsider H = H, G = G as Subset of X ;
( x0 in the carrier of X0 & the carrier of X0 c= the carrier of X ) by BORSUK_1:35;
then reconsider x = x0 as Point of X ;
((modid X,A) | X0) . x0 = (id the carrier of X) . x by FUNCT_1:72
.= x by FUNCT_1:35 ;
then ( ( x in H or x in G /\ A ) & x in A ) by A1, A2, A3, XBOOLE_0:def 3;
then ( x in H /\ A or x in G /\ A ) by XBOOLE_0:def 4;
then A5: x in (H /\ A) \/ (G /\ A) by XBOOLE_0:def 3;
A6: ((modid X,A) | X0) .: ((H \/ G) /\ A) = (id the carrier of X) .: ((H \/ G) /\ A) by A1, FUNCT_2:174, XBOOLE_1:17
.= (H \/ G) /\ A by FUNCT_1:162 ;
A7: (H /\ A) \/ (G /\ A) c= W by A3, XBOOLE_1:9, XBOOLE_1:17;
thus ex V being Subset of X0 st
( V is open & x0 in V & ((modid X,A) | X0) .: V c= W ) :: thesis: verum

proof

reconsider V = (H \/ G) /\ A as Subset of X0 by A1, XBOOLE_1:17;
take V ; :: thesis: ( V is open & x0 in V & ((modid X,A) | X0) .: V c= W )
( H is open & G is open ) by A4, PRE_TOPC:def 5;
then ( V = (H \/ G) /\ ([#] X0) & H \/ G is open ) by A1, TOPS_1:37;
hence ( V is open & x0 in V & ((modid X,A) | X0) .: V c= W ) by A5, A6, A7, TOPS_2:32, XBOOLE_1:23; :: thesis: verum

end;

end;

hence (modid X,A) | X0 is_continuous_at x0 by Th48; :: thesis: verum