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

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;