let X, Y be non empty TopSpace; :: thesis: for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for A being Subset of X0
for x0 being Point of X0
for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let X1, X0 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y st X1 is SubSpace of X0 holds
for A being Subset of X0
for x0 being Point of X0
for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let g be Function of X0,Y; :: thesis: ( X1 is SubSpace of X0 implies for A being Subset of X0
for x0 being Point of X0
for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )
assume A1: X1 is SubSpace of X0 ; :: thesis: for A being Subset of X0
for x0 being Point of X0
for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let A be Subset of X0; :: thesis: for x0 being Point of X0
for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let x0 be Point of X0; :: thesis: for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
let x1 be Point of X1; :: thesis: ( A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 implies ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 ) )
assume that
A2: A c= the carrier of X1 and
A3: A is a_neighborhood of x0 and
A4: x0 = x1 ; :: thesis: ( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
thus ( g is_continuous_at x0 implies g | X1 is_continuous_at x1 ) by A1, A4, Th81; :: thesis: ( g | X1 is_continuous_at x1 implies g is_continuous_at x0 )
thus ( g | X1 is_continuous_at x1 implies g is_continuous_at x0 ) :: thesis: verum

proof

assume A5: g | X1 is_continuous_at x1 ; :: thesis: g is_continuous_at x0
for G being Subset of Y st G is open & g . x0 in G holds
ex H being Subset of X0 st
( H is open & x0 in H & g .: H c= G )

proof

let G be Subset of Y; :: thesis: ( G is open & g . x0 in G implies ex H being Subset of X0 st
( H is open & x0 in H & g .: H c= G ) )
assume that
A6: G is open and
A7: g . x0 in G ; :: thesis: ex H being Subset of X0 st
( H is open & x0 in H & g .: H c= G )
(g | X1) . x1 in G by A1, A4, A7, Th72;
then consider H1 being Subset of X1 such that
A8: H1 is open and
A9: x1 in H1 and
A10: (g | X1) .: H1 c= G by A5, A6, Th48;
consider V being Subset of X0 such that
A11: V is open and
A12: V c= A and
A13: x0 in V by A3, CONNSP_2:8;
reconsider V1 = V as Subset of X1 by A2, A12, XBOOLE_1:1;
A14: H1 /\ V1 c= V by XBOOLE_1:17;
V1 is open by A1, A11, TOPS_2:33;
then A15: H1 /\ V1 is open by A8, TOPS_1:38;
reconsider H = H1 /\ V1 as Subset of X0 by A14, XBOOLE_1:1;
take H ; :: thesis: ( H is open & x0 in H & g .: H c= G )
for z being Point of Y st z in g .: H holds
z in G

proof

let z be Point of Y; :: thesis: ( z in g .: H implies z in G )
assume z in g .: H ; :: thesis: z in G
then consider y being Point of X0 such that
A16: y in H and
A17: z = g . y by FUNCT_2:116;
set f = g | X1;
y in V by A14, A16;
then y in A by A12;
then A18: z = (g | X1) . y by A1, A2, A17, Th72;
H1 /\ V1 c= H1 by XBOOLE_1:17;
then z in (g | X1) .: H1 by A16, A18, FUNCT_2:43;
hence z in G by A10; :: thesis: verum

end;

hence ( H is open & x0 in H & g .: H c= G ) by A1, A4, A9, A11, A13, A14, A15, SUBSET_1:7, TSEP_1:9, XBOOLE_0:def 4; :: thesis: verum

end;

hence g is_continuous_at x0 by Th48; :: thesis: verum

end;