let X, Y be non empty TopSpace; :: thesis: for X0, X1 being non empty SubSpace of X
for g being Function of X0,Y
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds
g | X1 is_continuous_at x1
let X0, X1 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds
g | X1 is_continuous_at x1
let g be Function of X0,Y; :: thesis: for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds
g | X1 is_continuous_at x1
let x0 be Point of X0; :: thesis: for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds
g | X1 is_continuous_at x1
let x1 be Point of X1; :: thesis: ( x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 implies g | X1 is_continuous_at x1 )
assume A1: x0 = x1 ; :: thesis: ( not X1 is SubSpace of X0 or not g is_continuous_at x0 or g | X1 is_continuous_at x1 )
assume A2: X1 is SubSpace of X0 ; :: thesis: ( not g is_continuous_at x0 or g | X1 is_continuous_at x1 )
assume A3: g is_continuous_at x0 ; :: thesis: g | X1 is_continuous_at x1
for G being Subset of Y st G is open & (g | X1) . x1 in G holds
ex H0 being Subset of X1 st
( H0 is open & x1 in H0 & (g | X1) .: H0 c= G )

proof

reconsider C = the carrier of X1 as Subset of X0 by A2, TSEP_1:1;
let G be Subset of Y; :: thesis: ( G is open & (g | X1) . x1 in G implies ex H0 being Subset of X1 st
( H0 is open & x1 in H0 & (g | X1) .: H0 c= G ) )
assume that
A4: G is open and
A5: (g | X1) . x1 in G ; :: thesis: ex H0 being Subset of X1 st
( H0 is open & x1 in H0 & (g | X1) .: H0 c= G )
g . x0 in G by A1, A2, A5, Th65;
then consider H being Subset of X0 such that
A6: ( H is open & x0 in H ) and
A7: g .: H c= G by A3, A4, Th43;
reconsider H0 = H /\ C as Subset of X1 by XBOOLE_1:17;
( g .: H0 c= (g .: H) /\ (g .: C) & (g .: H) /\ (g .: C) c= g .: H ) by RELAT_1:121, XBOOLE_1:17;
then g .: H0 c= g .: H by XBOOLE_1:1;
then A8: g .: H0 c= G by A7, XBOOLE_1:1;
take H0 ; :: thesis: ( H0 is open & x1 in H0 & (g | X1) .: H0 c= G )
g | X1 = g | C by A2, Def5;
then ( H0 = H /\ ([#] X1) & (g | X1) .: H0 c= g .: H0 ) by RELAT_1:128;
hence ( H0 is open & x1 in H0 & (g | X1) .: H0 c= G ) by A1, A2, A6, A8, TOPS_2:24, XBOOLE_0:def 4, XBOOLE_1:1; :: thesis: verum

end;

hence g | X1 is_continuous_at x1 by Th43; :: thesis: verum