let X be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum