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:17;
reconsider N2 =
N1 as
Subset of
RealSpace by TOPMETR:12, TOPMETR:17, TOPMETR:def 6;
N2 in Family_open_set RealSpace
by Lm3;
then
N2 in the
topology of
(TopSpaceMetr RealSpace)
by TOPMETR:12;
then
N19 is
open
by TOPMETR:def 6;
then reconsider G =
N19 as
a_neighborhood of
fx by A2, A3, CONNSP_2:3, RCOMP_1:16;
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:6;
reconsider V1 =
V as
Subset of
REAL by TOPMETR:17;
V in the
topology of
R^1
by A5;
then
V in Family_open_set RealSpace
by TOPMETR:12, TOPMETR:def 6;
then
V1 is
open
by Lm4;
then consider N being
Neighbourhood of
x1 such that A8:
N c= V1
by A3, A7, RCOMP_1:18;
N c= H
by A6, A8;
then
g .: N c= g .: H
by RELAT_1:123;
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