let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0)

let X0 be non empty SubSpace of X; :: thesis: (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0)

for x0 being Point of X0 holds (modid (X,X0)) | X0 is_continuous_at x0 by Th107;

hence (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0) by Th44; :: thesis: verum

let X0 be non empty SubSpace of X; :: thesis: (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0)

for x0 being Point of X0 holds (modid (X,X0)) | X0 is_continuous_at x0 by Th107;

hence (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0) by Th44; :: thesis: verum