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 A3, Th58; :: 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: f is_continuous_at x
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 A3, A6, FUNCT_1:49;
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 A2, CONNSP_2:6;
reconsider V0 = V as Subset of X0 by A1, A11, XBOOLE_1:1;
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 A13, A15;
then y in A by A11;
then A17: z = (f | X0) . y by A1, A16, FUNCT_1:49;
H0 /\ V0 c= H0 by XBOOLE_1:17;
then z in (f | X0) .: H0 by A15, A17, FUNCT_2:35;
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 A10, TOPS_2:25;
then H0 /\ V0 is open by A7;
hence ( H is open & x in H & f .: H c= G ) by A3, A8, A10, A12, A13, A14, SUBSET_1:2, TSEP_1:9, XBOOLE_0:def 4; :: thesis: verum

end;

hence f is_continuous_at x by Th43; :: thesis: verum

end;