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 ; :: 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 end;