let X, Y be non empty TopSpace; :: thesis: for X0, X1 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 X0, X1 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, Th74; :: 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:
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, Th65;
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, Th43;
consider V being Subset of X0 such that
A11: V is open and
A12: V c= A and
A13: x0 in V by ;
reconsider V1 = V as Subset of X1 by ;
A14: H1 /\ V1 c= V by XBOOLE_1:17;
then reconsider H = H1 /\ V1 as Subset of X0 by XBOOLE_1:1;
A15: for z being Point of Y st z in g .: H holds
z in G
proof
set f = g | X1;
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:65;
y in V by ;
then y in A by A12;
then A18: z = (g | X1) . y by A1, A2, A17, Th65;
H1 /\ V1 c= H1 by XBOOLE_1:17;
then z in (g | X1) .: H1 by ;
hence z in G by A10; :: thesis: verum
end;
take H ; :: thesis: ( H is open & x0 in H & g .: H c= G )
V1 is open by ;
then H1 /\ V1 is open by A8;
hence ( H is open & x0 in H & g .: H c= G ) by ; :: thesis: verum
end;
hence g is_continuous_at x0 by Th43; :: thesis: verum
end;