let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y

for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let f be Function of X,Y; :: thesis: for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X

for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let A be Subset of X; :: thesis: for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x be Point of X; :: thesis: for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x0 be Point of X0; :: thesis: ( A c= the carrier of X0 & A is a_neighborhood of x & x = x0 implies ( f is_continuous_at x iff f | X0 is_continuous_at x0 ) )

assume that

A1: A c= the carrier of X0 and

A2: A is a_neighborhood of x and

A3: x = x0 ; :: thesis: ( f is_continuous_at x iff f | X0 is_continuous_at x0 )

thus ( f is_continuous_at x implies f | X0 is_continuous_at x0 ) by A3, Th58; :: thesis: ( f | X0 is_continuous_at x0 implies f is_continuous_at x )

thus ( f | X0 is_continuous_at x0 implies f is_continuous_at x ) :: thesis: verum

for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let f be Function of X,Y; :: thesis: for X0 being non empty SubSpace of X

for A being Subset of X

for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X

for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let A be Subset of X; :: thesis: for x being Point of X

for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x be Point of X; :: thesis: for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x0 be Point of X0; :: thesis: ( A c= the carrier of X0 & A is a_neighborhood of x & x = x0 implies ( f is_continuous_at x iff f | X0 is_continuous_at x0 ) )

assume that

A1: A c= the carrier of X0 and

A2: A is a_neighborhood of x and

A3: x = x0 ; :: thesis: ( f is_continuous_at x iff f | X0 is_continuous_at x0 )

thus ( f is_continuous_at x implies f | X0 is_continuous_at x0 ) by A3, Th58; :: thesis: ( f | X0 is_continuous_at x0 implies f is_continuous_at x )

thus ( f | X0 is_continuous_at x0 implies f is_continuous_at x ) :: thesis: verum

proof

assume A4:
f | X0 is_continuous_at x0
; :: thesis: f is_continuous_at x

for G being Subset of Y st G is open & f . x in G holds

ex H being Subset of X st

( H is open & x in H & f .: H c= G )

end;for G being Subset of Y st G is open & f . x in G holds

ex H being Subset of X st

( H is open & x in H & f .: H c= G )

proof

hence
f is_continuous_at x
by Th43; :: thesis: verum
let G be Subset of Y; :: thesis: ( G is open & f . x in G implies ex H being Subset of X st

( H is open & x in H & f .: H c= G ) )

assume that

A5: G is open and

A6: f . x in G ; :: thesis: ex H being Subset of X st

( H is open & x in H & f .: H c= G )

(f | X0) . x0 in G by A3, A6, FUNCT_1:49;

then consider H0 being Subset of X0 such that

A7: H0 is open and

A8: x0 in H0 and

A9: (f | X0) .: H0 c= G by A4, A5, Th43;

consider V being Subset of X such that

A10: V is open and

A11: V c= A and

A12: x in V by A2, CONNSP_2:6;

reconsider V0 = V as Subset of X0 by A1, A11, XBOOLE_1:1;

A13: H0 /\ V0 c= V by XBOOLE_1:17;

then reconsider H = H0 /\ V0 as Subset of X by XBOOLE_1:1;

A14: for z being Point of Y st z in f .: H holds

z in G

V0 is open by A10, TOPS_2:25;

then H0 /\ V0 is open by A7;

hence ( H is open & x in H & f .: H c= G ) by A3, A8, A10, A12, A13, A14, SUBSET_1:2, TSEP_1:9, XBOOLE_0:def 4; :: thesis: verum

end;( H is open & x in H & f .: H c= G ) )

assume that

A5: G is open and

A6: f . x in G ; :: thesis: ex H being Subset of X st

( H is open & x in H & f .: H c= G )

(f | X0) . x0 in G by A3, A6, FUNCT_1:49;

then consider H0 being Subset of X0 such that

A7: H0 is open and

A8: x0 in H0 and

A9: (f | X0) .: H0 c= G by A4, A5, Th43;

consider V being Subset of X such that

A10: V is open and

A11: V c= A and

A12: x in V by A2, CONNSP_2:6;

reconsider V0 = V as Subset of X0 by A1, A11, XBOOLE_1:1;

A13: H0 /\ V0 c= V by XBOOLE_1:17;

then reconsider H = H0 /\ V0 as Subset of X by XBOOLE_1:1;

A14: for z being Point of Y st z in f .: H holds

z in G

proof

take
H
; :: thesis: ( H is open & x in H & f .: H c= G )
set g = f | X0;

let z be Point of Y; :: thesis: ( z in f .: H implies z in G )

assume z in f .: H ; :: thesis: z in G

then consider y being Point of X such that

A15: y in H and

A16: z = f . y by FUNCT_2:65;

y in V by A13, A15;

then y in A by A11;

then A17: z = (f | X0) . y by A1, A16, FUNCT_1:49;

H0 /\ V0 c= H0 by XBOOLE_1:17;

then z in (f | X0) .: H0 by A15, A17, FUNCT_2:35;

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

end;let z be Point of Y; :: thesis: ( z in f .: H implies z in G )

assume z in f .: H ; :: thesis: z in G

then consider y being Point of X such that

A15: y in H and

A16: z = f . y by FUNCT_2:65;

y in V by A13, A15;

then y in A by A11;

then A17: z = (f | X0) . y by A1, A16, FUNCT_1:49;

H0 /\ V0 c= H0 by XBOOLE_1:17;

then z in (f | X0) .: H0 by A15, A17, FUNCT_2:35;

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

V0 is open by A10, TOPS_2:25;

then H0 /\ V0 is open by A7;

hence ( H is open & x in H & f .: H c= G ) by A3, A8, A10, A12, A13, A14, SUBSET_1:2, TSEP_1:9, XBOOLE_0:def 4; :: thesis: verum