let X be non empty TopSpace; :: thesis: for A being Subset of X

for x being Point of X st not x in A holds

modid (X,A) is_continuous_at x

let A be Subset of X; :: thesis: for x being Point of X st not x in A holds

modid (X,A) is_continuous_at x

let x be Point of X; :: thesis: ( not x in A implies modid (X,A) is_continuous_at x )

assume A1: not x in A ; :: thesis: modid (X,A) is_continuous_at x

for x being Point of X st not x in A holds

modid (X,A) is_continuous_at x

let A be Subset of X; :: thesis: for x being Point of X st not x in A holds

modid (X,A) is_continuous_at x

let x be Point of X; :: thesis: ( not x in A implies modid (X,A) is_continuous_at x )

assume A1: not x in A ; :: thesis: modid (X,A) is_continuous_at x

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

ex V being Subset of X st

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

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

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

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

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

assume that

A2: W is open and

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

( V is open & x in V & (modid (X,A)) .: 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 and

G in the topology of X by A2;

A6: G /\ A c= A by XBOOLE_1:17;

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

thus ex V being Subset of X st

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

end;( V is open & x in V & (modid (X,A)) .: V c= W ) )

assume that

A2: W is open and

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

( V is open & x in V & (modid (X,A)) .: 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 and

G in the topology of X by A2;

A6: G /\ A c= A by XBOOLE_1:17;

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

thus ex V being Subset of X st

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