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

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

let A be Subset of X; :: thesis: for X0 being non empty SubSpace of X st the carrier of X0 misses A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

let X0 be non empty SubSpace of X; :: thesis: ( the carrier of X0 misses A implies for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0 )

assume A1: the carrier of X0 /\ A = {} ; :: according to XBOOLE_0:def 7 :: thesis: for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

let x0 be Point of X0; :: thesis: (modid (X,A)) | X0 is_continuous_at x0

( x0 in the carrier of X0 & the carrier of X0 c= the carrier of X ) by BORSUK_1:1;

then reconsider x = x0 as Point of X ;

not x in A by A1, XBOOLE_0:def 4;

hence (modid (X,A)) | X0 is_continuous_at x0 by Th58, Th96; :: thesis: verum

for X0 being non empty SubSpace of X st the carrier of X0 misses A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

let A be Subset of X; :: thesis: for X0 being non empty SubSpace of X st the carrier of X0 misses A holds

for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

let X0 be non empty SubSpace of X; :: thesis: ( the carrier of X0 misses A implies for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0 )

assume A1: the carrier of X0 /\ A = {} ; :: according to XBOOLE_0:def 7 :: thesis: for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0

let x0 be Point of X0; :: thesis: (modid (X,A)) | X0 is_continuous_at x0

( x0 in the carrier of X0 & the carrier of X0 c= the carrier of X ) by BORSUK_1:1;

then reconsider x = x0 as Point of X ;

not x in A by A1, XBOOLE_0:def 4;

hence (modid (X,A)) | X0 is_continuous_at x0 by Th58, Th96; :: thesis: verum