let f be Function of R^1 ,R^1 ; for x being Point of R^1
for g being PartFunc of REAL ,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let x be Point of R^1 ; for g being PartFunc of REAL ,REAL
for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let g be PartFunc of REAL ,REAL ; for x1 being Real st f is_continuous_at x & f = g & x = x1 holds
g is_continuous_in x1
let x1 be Real; ( f is_continuous_at x & f = g & x = x1 implies g is_continuous_in x1 )
assume that
A1:
f is_continuous_at x
and
A2:
f = g
and
A3:
x = x1
; g is_continuous_in x1
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1
proof
reconsider fx =
f . x as
Point of
R^1 ;
let N1 be
Neighbourhood of
g . x1;
ex N being Neighbourhood of x1 st g .: N c= N1
reconsider N19 =
N1 as
Subset of
R^1 by TOPMETR:24;
reconsider N2 =
N1 as
Subset of
RealSpace by TOPMETR:16, TOPMETR:24, TOPMETR:def 7;
N2 in Family_open_set RealSpace
by Lm3;
then
N2 in the
topology of
(TopSpaceMetr RealSpace )
by TOPMETR:16;
then
N19 is
open
by PRE_TOPC:def 5, TOPMETR:def 7;
then reconsider G =
N19 as
a_neighborhood of
fx by A2, A3, CONNSP_2:5, RCOMP_1:37;
consider H being
a_neighborhood of
x such that A4:
f .: H c= G
by A1, TMAP_1:def 2;
consider V being
Subset of
R^1 such that A5:
V is
open
and A6:
V c= H
and A7:
x in V
by CONNSP_2:8;
reconsider V1 =
V as
Subset of
REAL by TOPMETR:24;
V in the
topology of
R^1
by A5, PRE_TOPC:def 5;
then
V in Family_open_set RealSpace
by TOPMETR:16, TOPMETR:def 7;
then
V1 is
open
by Lm4;
then consider N being
Neighbourhood of
x1 such that A8:
N c= V1
by A3, A7, RCOMP_1:39;
N c= H
by A6, A8, XBOOLE_1:1;
then
g .: N c= g .: H
by RELAT_1:156;
hence
ex
N being
Neighbourhood of
x1 st
g .: N c= N1
by A2, A4, XBOOLE_1:1;
verum
end;
hence
g is_continuous_in x1
by FCONT_1:5; verum