let x0 be Real; :: 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 that

A1: f is_continuous_in x0 and

A2: f . x0 <> 0 ; :: thesis: 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; :: 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 that

A4: rng s1 c= dom (f ^) and

A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (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; :: thesis: (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 ;

:: thesis: verum

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 that

A1: f is_continuous_in x0 and

A2: f . x0 <> 0 ; :: thesis: 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; :: 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 that

A4: rng s1 c= dom (f ^) and

A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (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; :: thesis: (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 ;

:: thesis: verum