let X be non empty TopSpace; for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
(modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A)
let A be Subset of X; for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
(modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A)
let X0 be non empty SubSpace of X; ( the carrier of X0 misses A implies (modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A) )
assume
the carrier of X0 misses A
; (modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A)
then
for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0
by Th97;
hence
(modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A)
by Th44; verum