let x0 be real number ; :: thesis: 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 ; :: 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 X: x0 in dom f by FUNCT_1:def 4;
not f . x0 in {0 } by A1, TARSKI:def 1;
then not x0 in f " {0 } by FUNCT_1:def 13;
then x0 in (dom f) \ (f " {0 }) by X, XBOOLE_0:def 5;
then A3: x0 in dom (f ^ ) by RFUNCT_1:def 8;
A4: (dom f) \ (f " {0 }) c= dom f by XBOOLE_1:36;
let s1 be Real_Sequence; :: according to FCONT_1:def 1 :: 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 " {0 }) by RFUNCT_1:def 8;
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, Def1;
then (f /* s1) " is convergent by A1, A5, RFUNCT_2:26, SEQ_2:35;
hence (f ^ ) /* s1 is convergent by A5, RFUNCT_2:27; :: thesis: (f ^ ) . x0 = lim ((f ^ ) /* s1)
thus (f ^ ) . x0 = (f . x0) " by A3, RFUNCT_1:def 8
.= lim ((f /* s1) " ) by A1, A5, A6, RFUNCT_2:26, SEQ_2:36
.= lim ((f ^ ) /* s1) by A5, RFUNCT_2:27 ; :: thesis: verum