let x0 be Complex; for f being PartFunc of COMPLEX,COMPLEX st f is_continuous_in x0 & f /. x0 <> 0 holds
f ^ is_continuous_in x0
let f be PartFunc of COMPLEX,COMPLEX; ( 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 {0c}
by A2, TARSKI:def 1;
then A3:
not x0 in f " {0c}
by PARTFUN2:26;
x0 in dom f
by A1;
then
x0 in (dom f) \ (f " {0c})
by A3, XBOOLE_0:def 5;
hence A4:
x0 in dom (f ^)
by CFUNCT_1:def 2; CFCONT_1:def 1 for s1 being Complex_Sequence st rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 holds
( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) )
let s1 be Complex_Sequence; ( rng s1 c= dom (f ^) & s1 is convergent & lim s1 = x0 implies ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) ) )
assume that
A5:
rng s1 c= dom (f ^)
and
A6:
( s1 is convergent & lim s1 = x0 )
; ( (f ^) /* s1 is convergent & (f ^) /. x0 = lim ((f ^) /* s1) )
( (dom f) \ (f " {0c}) c= dom f & rng s1 c= (dom f) \ (f " {0c}) )
by A5, CFUNCT_1:def 2, XBOOLE_1:36;
then
rng s1 c= dom f
;
then A7:
( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
by A1, A6;
f /* s1 is non-zero
by A5, Th10;
then
(f /* s1) " is convergent
by A2, A7, COMSEQ_2:34;
hence
(f ^) /* s1 is convergent
by A5, Th11; (f ^) /. x0 = lim ((f ^) /* s1)
thus (f ^) /. x0 =
(f /. x0) "
by A4, CFUNCT_1:def 2
.=
lim ((f /* s1) ")
by A2, A5, A7, Th10, COMSEQ_2:35
.=
lim ((f ^) /* s1)
by A5, Th11
; verum