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

for X0 being non empty open SubSpace of X

for x being Point of X

for x0 being Point of X0 st 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 open SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let X0 be non empty open SubSpace of X; :: thesis: for x being Point of X

for x0 being Point of X0 st 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 x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x0 be Point of X0; :: thesis: ( x = x0 implies ( f is_continuous_at x iff f | X0 is_continuous_at x0 ) )

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

hence ( f is_continuous_at x implies f | X0 is_continuous_at x0 ) by 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 open SubSpace of X

for x being Point of X

for x0 being Point of X0 st 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 open SubSpace of X

for x being Point of X

for x0 being Point of X0 st x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let X0 be non empty open SubSpace of X; :: thesis: for x being Point of X

for x0 being Point of X0 st 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 x = x0 holds

( f is_continuous_at x iff f | X0 is_continuous_at x0 )

let x0 be Point of X0; :: thesis: ( x = x0 implies ( f is_continuous_at x iff f | X0 is_continuous_at x0 ) )

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

hence ( f is_continuous_at x implies f | X0 is_continuous_at x0 ) by 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

reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

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

A is open by TSEP_1:16;

hence f is_continuous_at x by A1, A2, Th60; :: thesis: verum

end;assume A2: f | X0 is_continuous_at x0 ; :: thesis: f is_continuous_at x

A is open by TSEP_1:16;

hence f is_continuous_at x by A1, A2, Th60; :: thesis: verum