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