let X be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X st X0 misses X1 holds

(modid (X,X0)) | X1 is continuous Function of X1,(X modified_with_respect_to X0)

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

assume X0 misses X1 ; :: thesis: (modid (X,X0)) | X1 is continuous Function of X1,(X modified_with_respect_to X0)

then for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1 by Th106;

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

(modid (X,X0)) | X1 is continuous Function of X1,(X modified_with_respect_to X0)

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

assume X0 misses X1 ; :: thesis: (modid (X,X0)) | X1 is continuous Function of X1,(X modified_with_respect_to X0)

then for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1 by Th106;

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