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
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider f = (modid (X,A)) | X0 as Function of X0,() by Def10;
let x0 be Point of X0; :: thesis: (modid (X,X0)) | X0 is_continuous_at x0
A1: (modid (X,A)) | X0 is_continuous_at x0 by Th98;
now :: thesis: for W being Subset of () st W is open & f . x0 in W holds
ex V being Subset of X0 st
( V is open & x0 in V & f .: V c= W )
let W be Subset of (); :: 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 ) )

reconsider W0 = W as Subset of () by Th102;
assume that
A2: W is open and
A3: f . x0 in W ; :: thesis: ex V being Subset of X0 st
( V is open & x0 in V & f .: V c= W )

W in the topology of () by A2;
then W in A -extension_of_the_topology_of X by Th102;
then A4: W0 is open ;
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, A3, A4, Th43;
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;
then f is_continuous_at x0 by Th43;
hence (modid (X,X0)) | X0 is_continuous_at x0 by Def11; :: thesis: verum