let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for x0 being Point of X0 holds (modid X,X0) | X0 is_continuous_at x0
let X0 be non empty SubSpace of X; :: thesis: for x0 being Point of X0 holds (modid X,X0) | X0 is_continuous_at x0
let x0 be Point of X0; :: thesis: (modid X,X0) | X0 is_continuous_at x0
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: (modid X,A) | X0 is_continuous_at x0 by Th110;
X modified_with_respect_to A = X modified_with_respect_to X0 by Def10;
then reconsider f = (modid X,A) | X0 as Function of X0,(X modified_with_respect_to X0) ;
f is_continuous_at x0

proof

now

let W be Subset of (X modified_with_respect_to X0); :: thesis: ( W is open & f . x0 in W implies ex V being Subset of X0 st
( V is open & x0 in V & f .: V c= W ) )
assume A2: ( W is open & f . x0 in W ) ; :: thesis: ex V being Subset of X0 st
( V is open & x0 in V & f .: V c= W )
then W in the topology of (X modified_with_respect_to X0) by PRE_TOPC:def 5;
then A3: W in A -extension_of_the_topology_of X by Th114;
reconsider W0 = W as Subset of (X modified_with_respect_to A) by Th114;
A4: W0 is open by A3, PRE_TOPC:def 5;
thus ex V being Subset of X0 st
( V is open & x0 in V & f .: V c= W ) :: thesis: verum

proof

consider V being Subset of X0 such that
A5: ( V is open & x0 in V & ((modid X,A) | X0) .: V c= W0 ) by A1, A2, A4, Th48;
take V ; :: thesis: ( V is open & x0 in V & f .: V c= W )
thus ( V is open & x0 in V & f .: V c= W ) by A5; :: thesis: verum

end;

end;

hence f is_continuous_at x0 by Th48; :: thesis: verum

end;

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