let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y
for X0 being non empty SubSpace of X
for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let f be Function of X,Y; :: thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let A be Subset of X; :: thesis: for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x be Point of X; :: thesis: for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x0 be Point of X0; :: thesis: ( A c= the carrier of X0 & A is a_neighborhood of x & x = x0 implies ( f is_continuous_at x iff f | X0 is_continuous_at x0 ) )
assume that
A1: A c= the carrier of X0 and
A2: A is a_neighborhood of x and
A3: x = x0 ; :: thesis: ( f is_continuous_at x iff f | X0 is_continuous_at x0 )
thus ( f is_continuous_at x implies f | X0 is_continuous_at x0 ) by ; :: thesis: ( f | X0 is_continuous_at x0 implies f is_continuous_at x )
thus ( f | X0 is_continuous_at x0 implies f is_continuous_at x ) :: thesis: verum
proof
assume A4: f | X0 is_continuous_at x0 ; :: thesis:
for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G )
proof
let G be Subset of Y; :: thesis: ( G is open & f . x in G implies ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )

assume that
A5: G is open and
A6: f . x in G ; :: thesis: ex H being Subset of X st
( H is open & x in H & f .: H c= G )

(f | X0) . x0 in G by ;
then consider H0 being Subset of X0 such that
A7: H0 is open and
A8: x0 in H0 and
A9: (f | X0) .: H0 c= G by A4, A5, Th43;
consider V being Subset of X such that
A10: V is open and
A11: V c= A and
A12: x in V by ;
reconsider V0 = V as Subset of X0 by ;
A13: H0 /\ V0 c= V by XBOOLE_1:17;
then reconsider H = H0 /\ V0 as Subset of X by XBOOLE_1:1;
A14: for z being Point of Y st z in f .: H holds
z in G
proof
set g = f | X0;
let z be Point of Y; :: thesis: ( z in f .: H implies z in G )
assume z in f .: H ; :: thesis: z in G
then consider y being Point of X such that
A15: y in H and
A16: z = f . y by FUNCT_2:65;
y in V by ;
then y in A by A11;
then A17: z = (f | X0) . y by ;
H0 /\ V0 c= H0 by XBOOLE_1:17;
then z in (f | X0) .: H0 by ;
hence z in G by A9; :: thesis: verum
end;
take H ; :: thesis: ( H is open & x in H & f .: H c= G )
V0 is open by ;
then H0 /\ V0 is open by A7;
hence ( H is open & x in H & f .: H c= G ) by ; :: thesis: verum
end;
hence f is_continuous_at x by Th43; :: thesis: verum
end;