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;

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

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 )

then
f is_continuous_at x1
by Th43;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

end;( 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

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