let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_right_differentiable_in x0 holds

f is_Rcontinuous_in x0

let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0 )

assume A1: f is_right_differentiable_in x0 ; :: thesis: f is_Rcontinuous_in x0

then consider r being Real such that

A2: r > 0 and

A3: [.x0,(x0 + r).] c= dom f ;

A4: for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) )

then x0 in [.x0,(x0 + r).] by XXREAL_1:1;

hence f is_Rcontinuous_in x0 by A3, A4; :: thesis: verum

f is_Rcontinuous_in x0

let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0 )

assume A1: f is_right_differentiable_in x0 ; :: thesis: f is_Rcontinuous_in x0

then consider r being Real such that

A2: r > 0 and

A3: [.x0,(x0 + r).] c= dom f ;

A4: for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) )

proof

x0 + 0 <= x0 + r
by A2, XREAL_1:7;
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;

set b = seq_const x0;

let a be Real_Sequence; :: thesis: ( rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 implies ( f /* a is convergent & f . x0 = lim (f /* a) ) )

assume that

A5: rng a c= (right_open_halfline x0) /\ (dom f) and

A6: a is convergent and

A7: lim a = x0 ; :: thesis: ( f /* a is convergent & f . x0 = lim (f /* a) )

consider r being Real such that

A8: r > 0 and

A9: [.x0,(x0 + r).] c= dom f by A1;

x0 + 0 < x0 + r by A8, XREAL_1:6;

then consider n0 being Nat such that

A10: for k being Nat st k >= n0 holds

a . k < x0 + r by A6, A7, LIMFUNC2:2;

deffunc H_{1}( Nat) -> set = (a . $1) - ((seq_const x0) . $1);

consider d being Real_Sequence such that

A11: for n being Nat holds d . n = H_{1}(n)
from SEQ_1:sch 1();

A12: d = a - (seq_const x0) by A11, RFUNCT_2:1;

then A13: d is convergent by A6;

reconsider c = (seq_const x0) ^\ n0 as constant Real_Sequence ;

A14: rng c = {x0}

lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26

.= x0 by SEQ_1:57 ;

then lim d = x0 - x0 by A6, A7, A12, SEQ_2:12

.= 0 ;

then A21: lim (d ^\ n0) = 0 by A13, SEQ_4:20;

A22: for n being Element of NAT holds

( d . n > 0 & d . n <> 0 )

then d ^\ n0 is non-zero by SEQ_1:5;

then reconsider h = d ^\ n0 as non-zero 0 -convergent Real_Sequence by A13, A21, FDIFF_1:def 1;

A27: rng a c= dom f by A5, XBOOLE_0:def 4;

.= (f /* a) ^\ n0 by A27, VALUED_0:27 ;

A30: for n being Element of NAT holds (a ^\ n0) . n in [.x0,(x0 + r).]

then A33: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A25, A14;

then A34: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A21, SEQ_2:15

.= 0 ;

then A37: (f /* (h + c)) - (f /* c) is convergent by A33;

then A38: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A20;

hence f /* a is convergent by A29, SEQ_4:21; :: thesis: f . x0 = lim (f /* a)

lim (f /* c) = f . x0 by A17, A20, SEQ_2:def 7;

then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0 + (f . x0) by A34, A36, A37, A20, SEQ_2:6

.= f . x0 ;

hence f . x0 = lim (f /* a) by A38, A29, SEQ_4:22; :: thesis: verum

end;set b = seq_const x0;

let a be Real_Sequence; :: thesis: ( rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 implies ( f /* a is convergent & f . x0 = lim (f /* a) ) )

assume that

A5: rng a c= (right_open_halfline x0) /\ (dom f) and

A6: a is convergent and

A7: lim a = x0 ; :: thesis: ( f /* a is convergent & f . x0 = lim (f /* a) )

consider r being Real such that

A8: r > 0 and

A9: [.x0,(x0 + r).] c= dom f by A1;

x0 + 0 < x0 + r by A8, XREAL_1:6;

then consider n0 being Nat such that

A10: for k being Nat st k >= n0 holds

a . k < x0 + r by A6, A7, LIMFUNC2:2;

deffunc H

consider d being Real_Sequence such that

A11: for n being Nat holds d . n = H

A12: d = a - (seq_const x0) by A11, RFUNCT_2:1;

then A13: d is convergent by A6;

reconsider c = (seq_const x0) ^\ n0 as constant Real_Sequence ;

A14: rng c = {x0}

proof

thus
rng c c= {x0}
:: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng c

assume x in {x0} ; :: thesis: x in rng c

then A16: x = x0 by TARSKI:def 1;

c . 0 = (seq_const x0) . (0 + n0) by NAT_1:def 3

.= x by A16, SEQ_1:57 ;

hence x in rng c by VALUED_0:28; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng c )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in {x0} )

assume x in rng c ; :: thesis: x in {x0}

then consider n being Element of NAT such that

A15: x = ((seq_const x0) ^\ n0) . n by FUNCT_2:113;

x = (seq_const x0) . (n + n0) by A15, NAT_1:def 3;

then x = x0 by SEQ_1:57;

hence x in {x0} by TARSKI:def 1; :: thesis: verum

end;assume x in rng c ; :: thesis: x in {x0}

then consider n being Element of NAT such that

A15: x = ((seq_const x0) ^\ n0) . n by FUNCT_2:113;

x = (seq_const x0) . (n + n0) by A15, NAT_1:def 3;

then x = x0 by SEQ_1:57;

hence x in {x0} by TARSKI:def 1; :: thesis: verum

assume x in {x0} ; :: thesis: x in rng c

then A16: x = x0 by TARSKI:def 1;

c . 0 = (seq_const x0) . (0 + n0) by NAT_1:def 3

.= x by A16, SEQ_1:57 ;

hence x in rng c by VALUED_0:28; :: thesis: verum

A17: now :: thesis: for g being Real st 0 < g holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g

then A20:
f /* c is convergent
by SEQ_2:def 6;ex n being Nat st

for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st

for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g )

assume A18: 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g

let m be Nat; :: thesis: ( n <= m implies |.(((f /* c) . m) - (f . x0)).| < g )

assume n <= m ; :: thesis: |.(((f /* c) . m) - (f . x0)).| < g

A19: m in NAT by ORDINAL1:def 12;

x0 + 0 <= x0 + r by A8, XREAL_1:7;

then x0 in [.x0,(x0 + r).] by XXREAL_1:1;

then rng c c= dom f by A9, A14, ZFMISC_1:31;

then |.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by FUNCT_2:108, A19

.= |.((f . ((seq_const x0) . (m + n0))) - (f . x0)).| by NAT_1:def 3

.= |.((f . x0) - (f . x0)).| by SEQ_1:57

.= 0 by ABSVALUE:2 ;

hence |.(((f /* c) . m) - (f . x0)).| < g by A18; :: thesis: verum

end;for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g )

assume A18: 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.(((f /* c) . m) - (f . x0)).| < g

let m be Nat; :: thesis: ( n <= m implies |.(((f /* c) . m) - (f . x0)).| < g )

assume n <= m ; :: thesis: |.(((f /* c) . m) - (f . x0)).| < g

A19: m in NAT by ORDINAL1:def 12;

x0 + 0 <= x0 + r by A8, XREAL_1:7;

then x0 in [.x0,(x0 + r).] by XXREAL_1:1;

then rng c c= dom f by A9, A14, ZFMISC_1:31;

then |.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by FUNCT_2:108, A19

.= |.((f . ((seq_const x0) . (m + n0))) - (f . x0)).| by NAT_1:def 3

.= |.((f . x0) - (f . x0)).| by SEQ_1:57

.= 0 by ABSVALUE:2 ;

hence |.(((f /* c) . m) - (f . x0)).| < g by A18; :: thesis: verum

lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26

.= x0 by SEQ_1:57 ;

then lim d = x0 - x0 by A6, A7, A12, SEQ_2:12

.= 0 ;

then A21: lim (d ^\ n0) = 0 by A13, SEQ_4:20;

A22: for n being Element of NAT holds

( d . n > 0 & d . n <> 0 )

proof

A25:
for n being Nat holds (d ^\ n0) . n > 0
let n be Element of NAT ; :: thesis: ( d . n > 0 & d . n <> 0 )

A23: d . n = (a . n) - ((seq_const x0) . n) by A11;

a . n in rng a by VALUED_0:28;

then a . n in right_open_halfline x0 by A5, XBOOLE_0:def 4;

then a . n in { r1 where r1 is Real : x0 < r1 } by XXREAL_1:230;

then A24: ex r1 being Real st

( r1 = a . n & x0 < r1 ) ;

then (a . n) - x0 > x0 - x0 by XREAL_1:9;

hence d . n > 0 by A23, SEQ_1:57; :: thesis: d . n <> 0

thus d . n <> 0 by A23, A24, SEQ_1:57; :: thesis: verum

end;A23: d . n = (a . n) - ((seq_const x0) . n) by A11;

a . n in rng a by VALUED_0:28;

then a . n in right_open_halfline x0 by A5, XBOOLE_0:def 4;

then a . n in { r1 where r1 is Real : x0 < r1 } by XXREAL_1:230;

then A24: ex r1 being Real st

( r1 = a . n & x0 < r1 ) ;

then (a . n) - x0 > x0 - x0 by XREAL_1:9;

hence d . n > 0 by A23, SEQ_1:57; :: thesis: d . n <> 0

thus d . n <> 0 by A23, A24, SEQ_1:57; :: thesis: verum

proof

for n being Nat holds (d ^\ n0) . n <> 0
by A25;
let n be Nat; :: thesis: (d ^\ n0) . n > 0

A26: n + n0 in NAT by ORDINAL1:def 12;

(d ^\ n0) . n = d . (n + n0) by NAT_1:def 3;

hence (d ^\ n0) . n > 0 by A22, A26; :: thesis: verum

end;A26: n + n0 in NAT by ORDINAL1:def 12;

(d ^\ n0) . n = d . (n + n0) by NAT_1:def 3;

hence (d ^\ n0) . n > 0 by A22, A26; :: thesis: verum

then d ^\ n0 is non-zero by SEQ_1:5;

then reconsider h = d ^\ n0 as non-zero 0 -convergent Real_Sequence by A13, A21, FDIFF_1:def 1;

A27: rng a c= dom f by A5, XBOOLE_0:def 4;

now :: thesis: for n being Element of NAT holds (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n

then A28:
((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c)
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n

thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by SEQ_1:7

.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by RFUNCT_2:1

.= (f /* (h + c)) . n ; :: thesis: verum

end;thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by SEQ_1:7

.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by RFUNCT_2:1

.= (f /* (h + c)) . n ; :: thesis: verum

now :: thesis: for n being Element of NAT holds (h + c) . n = (a ^\ n0) . n

then A29: ((f /* (h + c)) - (f /* c)) + (f /* c) =
f /* (a ^\ n0)
by A28, FUNCT_2:63
let n be Element of NAT ; :: thesis: (h + c) . n = (a ^\ n0) . n

thus (h + c) . n = (((a - (seq_const x0)) + (seq_const x0)) ^\ n0) . n by A12, SEQM_3:15

.= ((a - (seq_const x0)) + (seq_const x0)) . (n + n0) by NAT_1:def 3

.= ((a - (seq_const x0)) . (n + n0)) + ((seq_const x0) . (n + n0)) by SEQ_1:7

.= ((a . (n + n0)) - ((seq_const x0) . (n + n0))) + ((seq_const x0) . (n + n0)) by RFUNCT_2:1

.= (a ^\ n0) . n by NAT_1:def 3 ; :: thesis: verum

end;thus (h + c) . n = (((a - (seq_const x0)) + (seq_const x0)) ^\ n0) . n by A12, SEQM_3:15

.= ((a - (seq_const x0)) + (seq_const x0)) . (n + n0) by NAT_1:def 3

.= ((a - (seq_const x0)) . (n + n0)) + ((seq_const x0) . (n + n0)) by SEQ_1:7

.= ((a . (n + n0)) - ((seq_const x0) . (n + n0))) + ((seq_const x0) . (n + n0)) by RFUNCT_2:1

.= (a ^\ n0) . n by NAT_1:def 3 ; :: thesis: verum

.= (f /* a) ^\ n0 by A27, VALUED_0:27 ;

A30: for n being Element of NAT holds (a ^\ n0) . n in [.x0,(x0 + r).]

proof

rng (h + c) c= [.x0,(x0 + r).]
let n be Element of NAT ; :: thesis: (a ^\ n0) . n in [.x0,(x0 + r).]

a . (n + n0) in rng a by VALUED_0:28;

then (a ^\ n0) . n in rng a by NAT_1:def 3;

then (a ^\ n0) . n in right_open_halfline x0 by A5, XBOOLE_0:def 4;

then (a ^\ n0) . n in { g where g is Real : x0 < g } by XXREAL_1:230;

then A31: ex g being Real st

( g = (a ^\ n0) . n & x0 < g ) ;

( 0 <= n & 0 + n0 = n0 ) ;

then n0 <= n0 + n by XREAL_1:6;

then a . (n + n0) <= x0 + r by A10;

then (a ^\ n0) . n <= x0 + r by NAT_1:def 3;

then (a ^\ n0) . n in { g where g is Real : ( x0 <= g & g <= x0 + r ) } by A31;

hence (a ^\ n0) . n in [.x0,(x0 + r).] by RCOMP_1:def 1; :: thesis: verum

end;a . (n + n0) in rng a by VALUED_0:28;

then (a ^\ n0) . n in rng a by NAT_1:def 3;

then (a ^\ n0) . n in right_open_halfline x0 by A5, XBOOLE_0:def 4;

then (a ^\ n0) . n in { g where g is Real : x0 < g } by XXREAL_1:230;

then A31: ex g being Real st

( g = (a ^\ n0) . n & x0 < g ) ;

( 0 <= n & 0 + n0 = n0 ) ;

then n0 <= n0 + n by XREAL_1:6;

then a . (n + n0) <= x0 + r by A10;

then (a ^\ n0) . n <= x0 + r by NAT_1:def 3;

then (a ^\ n0) . n in { g where g is Real : ( x0 <= g & g <= x0 + r ) } by A31;

hence (a ^\ n0) . n in [.x0,(x0 + r).] by RCOMP_1:def 1; :: thesis: verum

proof

then
rng (h + c) c= dom f
by A9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (h + c) or x in [.x0,(x0 + r).] )

assume x in rng (h + c) ; :: thesis: x in [.x0,(x0 + r).]

then consider n being Element of NAT such that

A32: x = (h + c) . n by FUNCT_2:113;

(h + c) . n = (((a - (seq_const x0)) + (seq_const x0)) ^\ n0) . n by A12, SEQM_3:15

.= ((a - (seq_const x0)) + (seq_const x0)) . (n + n0) by NAT_1:def 3

.= ((a - (seq_const x0)) . (n + n0)) + ((seq_const x0) . (n + n0)) by SEQ_1:7

.= ((a . (n + n0)) - ((seq_const x0) . (n + n0))) + ((seq_const x0) . (n + n0)) by RFUNCT_2:1

.= (a ^\ n0) . n by NAT_1:def 3 ;

hence x in [.x0,(x0 + r).] by A30, A32; :: thesis: verum

end;assume x in rng (h + c) ; :: thesis: x in [.x0,(x0 + r).]

then consider n being Element of NAT such that

A32: x = (h + c) . n by FUNCT_2:113;

(h + c) . n = (((a - (seq_const x0)) + (seq_const x0)) ^\ n0) . n by A12, SEQM_3:15

.= ((a - (seq_const x0)) + (seq_const x0)) . (n + n0) by NAT_1:def 3

.= ((a - (seq_const x0)) . (n + n0)) + ((seq_const x0) . (n + n0)) by SEQ_1:7

.= ((a . (n + n0)) - ((seq_const x0) . (n + n0))) + ((seq_const x0) . (n + n0)) by RFUNCT_2:1

.= (a ^\ n0) . n by NAT_1:def 3 ;

hence x in [.x0,(x0 + r).] by A30, A32; :: thesis: verum

then A33: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A25, A14;

then A34: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A21, SEQ_2:15

.= 0 ;

now :: thesis: for n being Element of NAT holds (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n

then A36:
h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c)
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n

A35: h . n <> 0 by A25;

thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by SEQ_1:8

.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by SEQ_1:8

.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10

.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n)

.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A35, XCMPLX_0:def 7

.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum

end;A35: h . n <> 0 by A25;

thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by SEQ_1:8

.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by SEQ_1:8

.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10

.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n)

.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A35, XCMPLX_0:def 7

.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum

then A37: (f /* (h + c)) - (f /* c) is convergent by A33;

then A38: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A20;

hence f /* a is convergent by A29, SEQ_4:21; :: thesis: f . x0 = lim (f /* a)

lim (f /* c) = f . x0 by A17, A20, SEQ_2:def 7;

then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0 + (f . x0) by A34, A36, A37, A20, SEQ_2:6

.= f . x0 ;

hence f . x0 = lim (f /* a) by A38, A29, SEQ_4:22; :: thesis: verum

then x0 in [.x0,(x0 + r).] by XXREAL_1:1;

hence f is_Rcontinuous_in x0 by A3, A4; :: thesis: verum