let x0 be Element of COMPLEX ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: f ^ is_continuous_in x0
not f /. x0 in {0c } by A2, TARSKI:def 1;
then A3: not x0 in f " {0c } by PARTFUN2:44;
x0 in dom f by A1, Def2;
then x0 in (dom f) \ (f " {0c }) by A3, XBOOLE_0:def 5;
hence A4: x0 in dom (f ^ ) by CFUNCT_1:def 2; :: according to CFCONT_1:def 2 :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( (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 by XBOOLE_1:1;
then A7: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A6, Def2;
then (f /* s1) " is convergent by A2, A5, Th21, COMSEQ_2:34;
hence (f ^ ) /* s1 is convergent by A5, Th22; :: thesis: (f ^ ) /. x0 = lim ((f ^ ) /* s1)
thus (f ^ ) /. x0 = (f /. x0) " by A4, CFUNCT_1:def 2
.= lim ((f /* s1) " ) by A2, A5, A7, Th21, COMSEQ_2:35
.= lim ((f ^ ) /* s1) by A5, Th22 ; :: thesis: verum