let X be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X st X0 misses X1 holds
for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1
let X0, X1 be non empty SubSpace of X; :: thesis: ( X0 misses X1 implies for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider f = (modid (X,A)) | X1 as Function of X1,(X modified_with_respect_to X0) by Def10;
assume A1: X0 misses X1 ; :: thesis: for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1
let x1 be Point of X1; :: thesis: (modid (X,X0)) | X1 is_continuous_at x1
the carrier of X1 misses A by A1, TSEP_1:def 3;
then A2: (modid (X,A)) | X1 is_continuous_at x1 by Th97;
now :: thesis: for W being Subset of (X modified_with_respect_to X0) st W is open & f . x1 in W holds
ex V being Subset of X1 st
( V is open & x1 in V & f .: V c= W )
let W be Subset of (X modified_with_respect_to X0); :: thesis: ( W is open & f . x1 in W implies ex V being Subset of X1 st
( V is open & x1 in V & f .: V c= W ) )
reconsider W0 = W as Subset of (X modified_with_respect_to A) by Th102;
assume that
A3: W is open and
A4: f . x1 in W ; :: thesis: ex V being Subset of X1 st
( V is open & x1 in V & f .: V c= W )
W in the topology of (X modified_with_respect_to X0) by A3;
then W in A -extension_of_the_topology_of X by Th102;
then A5: W0 is open ;
thus ex V being Subset of X1 st
( V is open & x1 in V & f .: V c= W ) :: thesis: verum
proof
consider V being Subset of X1 such that
A6: ( V is open & x1 in V & ((modid (X,A)) | X1) .: V c= W0 ) by A2, A4, A5, Th43;
take V ; :: thesis: ( V is open & x1 in V & f .: V c= W )
thus ( V is open & x1 in V & f .: V c= W ) by A6; :: thesis: verum
end;
end;
then f is_continuous_at x1 by Th43;
hence (modid (X,X0)) | X1 is_continuous_at x1 by Def11; :: thesis: verum