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 = 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 = 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 = A implies for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0 )

assume A1: the carrier of X0 = A ; :: 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

for X0 being non empty SubSpace of X st the carrier of X0 = 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 = 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 = A implies for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0 )

assume A1: the carrier of X0 = A ; :: 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

now :: thesis: for W being Subset of (X modified_with_respect_to A) st W is open & ((modid (X,A)) | X0) . x0 in W holds

ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W )

hence
(modid (X,A)) | X0 is_continuous_at x0
by Th43; :: thesis: verumex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W )

( 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 ;

let W be Subset of (X modified_with_respect_to A); :: thesis: ( W is open & ((modid (X,A)) | X0) . x0 in W implies ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W ) )

assume that

A2: W is open and

A3: ((modid (X,A)) | X0) . x0 in W ; :: thesis: ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W )

consider H, G being Subset of X such that

A4: W = H \/ (G /\ A) and

A5: ( H in the topology of X & G in the topology of X ) by A2;

reconsider H = H, G = G as Subset of X ;

A6: (H /\ A) \/ (G /\ A) c= W by A4, XBOOLE_1:9, XBOOLE_1:17;

((modid (X,A)) | X0) . x0 = (id the carrier of X) . x by FUNCT_1:49

.= x ;

then ( x in H or x in G /\ A ) by A3, A4, XBOOLE_0:def 3;

then ( x in H /\ A or x in G /\ A ) by A1, XBOOLE_0:def 4;

then A7: x in (H /\ A) \/ (G /\ A) by XBOOLE_0:def 3;

A8: ((modid (X,A)) | X0) .: ((H \/ G) /\ A) = (id the carrier of X) .: ((H \/ G) /\ A) by A1, FUNCT_2:97, XBOOLE_1:17

.= (H \/ G) /\ A by FUNCT_1:92 ;

thus ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W ) :: thesis: verum

end;then reconsider x = x0 as Point of X ;

let W be Subset of (X modified_with_respect_to A); :: thesis: ( W is open & ((modid (X,A)) | X0) . x0 in W implies ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W ) )

assume that

A2: W is open and

A3: ((modid (X,A)) | X0) . x0 in W ; :: thesis: ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W )

consider H, G being Subset of X such that

A4: W = H \/ (G /\ A) and

A5: ( H in the topology of X & G in the topology of X ) by A2;

reconsider H = H, G = G as Subset of X ;

A6: (H /\ A) \/ (G /\ A) c= W by A4, XBOOLE_1:9, XBOOLE_1:17;

((modid (X,A)) | X0) . x0 = (id the carrier of X) . x by FUNCT_1:49

.= x ;

then ( x in H or x in G /\ A ) by A3, A4, XBOOLE_0:def 3;

then ( x in H /\ A or x in G /\ A ) by A1, XBOOLE_0:def 4;

then A7: x in (H /\ A) \/ (G /\ A) by XBOOLE_0:def 3;

A8: ((modid (X,A)) | X0) .: ((H \/ G) /\ A) = (id the carrier of X) .: ((H \/ G) /\ A) by A1, FUNCT_2:97, XBOOLE_1:17

.= (H \/ G) /\ A by FUNCT_1:92 ;

thus ex V being Subset of X0 st

( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W ) :: thesis: verum

proof

reconsider V = (H \/ G) /\ A as Subset of X0 by A1, XBOOLE_1:17;

take V ; :: thesis: ( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W )

( H is open & G is open ) by A5;

then A9: H \/ G is open ;

V = (H \/ G) /\ ([#] X0) by A1;

hence ( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W ) by A7, A8, A6, A9, TOPS_2:24, XBOOLE_1:23; :: thesis: verum

end;take V ; :: thesis: ( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W )

( H is open & G is open ) by A5;

then A9: H \/ G is open ;

V = (H \/ G) /\ ([#] X0) by A1;

hence ( V is open & x0 in V & ((modid (X,A)) | X0) .: V c= W ) by A7, A8, A6, A9, TOPS_2:24, XBOOLE_1:23; :: thesis: verum