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 )

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

hence
g | X1 is_continuous_at x1
by Th43; :: thesis: verum
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;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