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

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: 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 )

end;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

hence
g is_continuous_at x0
by Th43; :: thesis: verum
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 A3, CONNSP_2:6;

reconsider V1 = V as Subset of X1 by A2, A12, XBOOLE_1:1;

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

V1 is open by A1, A11, TOPS_2:25;

then H1 /\ V1 is open by A8;

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

end;( 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 A3, CONNSP_2:6;

reconsider V1 = V as Subset of X1 by A2, A12, XBOOLE_1:1;

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

take
H
; :: thesis: ( H is open & x0 in H & g .: H c= G )
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 A14, A16;

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 A16, A18, FUNCT_2:35;

hence z in G by A10; :: thesis: verum

end;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 A14, A16;

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 A16, A18, FUNCT_2:35;

hence z in G by A10; :: thesis: verum

V1 is open by A1, A11, TOPS_2:25;

then H1 /\ V1 is open by A8;

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