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

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;