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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

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

assume that

A1: ( A is open & x in A ) and

A2: A c= the carrier of X0 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & 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 is open & x in A & A c= the carrier of X0 & x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

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

assume that

A1: ( A is open & x in A ) and

A2: A c= the carrier of X0 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

A is a_neighborhood of x by A1, CONNSP_2:3;

hence f is_continuous_at x by A2, A3, A4, Th59; :: thesis: verum

end;A is a_neighborhood of x by A1, CONNSP_2:3;

hence f is_continuous_at x by A2, A3, A4, Th59; :: thesis: verum