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 )
proof
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 ;
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 ;
then f .: H0 c= f .: H by XBOOLE_1:1;
then A7: f .: H0 c= G by ;
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 ; :: thesis: verum
end;
hence f | X0 is_continuous_at x0 by Th43; :: thesis: verum