let x0 be Real; for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds
f ^ is_continuous_in x0
let f be PartFunc of REAL,REAL; ( f is_continuous_in x0 & f . x0 <> 0 implies f ^ is_continuous_in x0 )
assume that
A1:
f is_continuous_in x0
and
A2:
f . x0 <> 0
; f ^ is_continuous_in x0
not f . x0 in {0}
by A2, TARSKI:def 1;
then A3:
not x0 in f " {0}
by FUNCT_1:def 7;
let s1 be Real_Sequence; FCONT_1:def 1 ( rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 implies ( (f ^) /* s1 is convergent & (f ^) . x0 = lim ((f ^) /* s1) ) )
assume that
A4:
rng s1 c= dom (f ^)
and
A5:
( s1 is convergent & lim s1 = x0 )
; ( (f ^) /* s1 is convergent & (f ^) . x0 = lim ((f ^) /* s1) )
( (dom f) \ (f " {0}) c= dom f & rng s1 c= (dom f) \ (f " {0}) )
by A4, RFUNCT_1:def 2, XBOOLE_1:36;
then
rng s1 c= dom f
;
then A6:
( f /* s1 is convergent & f . x0 = lim (f /* s1) )
by A1, A5;
then
(f /* s1) " is convergent
by A2, A4, RFUNCT_2:11, SEQ_2:21;
hence
(f ^) /* s1 is convergent
by A4, RFUNCT_2:12; (f ^) . x0 = lim ((f ^) /* s1)
x0 in dom f
by A2, FUNCT_1:def 2;
then
x0 in (dom f) \ (f " {0})
by A3, XBOOLE_0:def 5;
then
x0 in dom (f ^)
by RFUNCT_1:def 2;
hence (f ^) . x0 =
(f . x0) "
by RFUNCT_1:def 2
.=
lim ((f /* s1) ")
by A2, A4, A6, RFUNCT_2:11, SEQ_2:22
.=
lim ((f ^) /* s1)
by A4, RFUNCT_2:12
;
verum