let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y

for X0 being non empty SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let f be Function of X,Y; :: thesis: for X0 being non empty SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let X0 be non empty SubSpace of X; :: thesis: for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let x be Point of X; :: thesis: for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let x0 be Point of X0; :: thesis: ( x = x0 & f is_continuous_at x implies f | X0 is_continuous_at x0 )

assume A1: x = x0 ; :: thesis: ( not f is_continuous_at x or f | X0 is_continuous_at x0 )

assume A2: f is_continuous_at x ; :: thesis: f | X0 is_continuous_at x0

for G being Subset of Y st G is open & (f | X0) . x0 in G holds

ex H0 being Subset of X0 st

( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )

for X0 being non empty SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let f be Function of X,Y; :: thesis: for X0 being non empty SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let X0 be non empty SubSpace of X; :: thesis: for x being Point of X

for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let x be Point of X; :: thesis: for x0 being Point of X0 st x = x0 & f is_continuous_at x holds

f | X0 is_continuous_at x0

let x0 be Point of X0; :: thesis: ( x = x0 & f is_continuous_at x implies f | X0 is_continuous_at x0 )

assume A1: x = x0 ; :: thesis: ( not f is_continuous_at x or f | X0 is_continuous_at x0 )

assume A2: f is_continuous_at x ; :: thesis: f | X0 is_continuous_at x0

for G being Subset of Y st G is open & (f | X0) . x0 in G holds

ex H0 being Subset of X0 st

( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )

proof

hence
f | X0 is_continuous_at x0
by Th43; :: thesis: verum
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;

let G be Subset of Y; :: thesis: ( G is open & (f | X0) . x0 in G implies ex H0 being Subset of X0 st

( H0 is open & x0 in H0 & (f | X0) .: H0 c= G ) )

assume that

A3: G is open and

A4: (f | X0) . x0 in G ; :: thesis: ex H0 being Subset of X0 st

( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )

f . x in G by A1, A4, FUNCT_1:49;

then consider H being Subset of X such that

A5: ( H is open & x in H ) and

A6: f .: H c= G by A2, A3, Th43;

reconsider H0 = H /\ C as Subset of X0 by XBOOLE_1:17;

( f .: H0 c= (f .: H) /\ (f .: C) & (f .: H) /\ (f .: C) c= f .: H ) by RELAT_1:121, XBOOLE_1:17;

then f .: H0 c= f .: H by XBOOLE_1:1;

then A7: f .: H0 c= G by A6, XBOOLE_1:1;

take H0 ; :: thesis: ( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )

( H0 = H /\ ([#] X0) & (f | X0) .: H0 c= f .: H0 ) by RELAT_1:128;

hence ( H0 is open & x0 in H0 & (f | X0) .: H0 c= G ) by A1, A5, A7, TOPS_2:24, XBOOLE_0:def 4, XBOOLE_1:1; :: thesis: verum

end;let G be Subset of Y; :: thesis: ( G is open & (f | X0) . x0 in G implies ex H0 being Subset of X0 st

( H0 is open & x0 in H0 & (f | X0) .: H0 c= G ) )

assume that

A3: G is open and

A4: (f | X0) . x0 in G ; :: thesis: ex H0 being Subset of X0 st

( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )

f . x in G by A1, A4, FUNCT_1:49;

then consider H being Subset of X such that

A5: ( H is open & x in H ) and

A6: f .: H c= G by A2, A3, Th43;

reconsider H0 = H /\ C as Subset of X0 by XBOOLE_1:17;

( f .: H0 c= (f .: H) /\ (f .: C) & (f .: H) /\ (f .: C) c= f .: H ) by RELAT_1:121, XBOOLE_1:17;

then f .: H0 c= f .: H by XBOOLE_1:1;

then A7: f .: H0 c= G by A6, XBOOLE_1:1;

take H0 ; :: thesis: ( H0 is open & x0 in H0 & (f | X0) .: H0 c= G )

( H0 = H /\ ([#] X0) & (f | X0) .: H0 c= f .: H0 ) by RELAT_1:128;

hence ( H0 is open & x0 in H0 & (f | X0) .: H0 c= G ) by A1, A5, A7, TOPS_2:24, XBOOLE_0:def 4, XBOOLE_1:1; :: thesis: verum