let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff (f,x0) = Ldiff (f,x0) holds

( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff (f,x0) = Ldiff (f,x0) implies ( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) ) )

assume that

A1: f is_right_differentiable_in x0 and

A2: f is_left_differentiable_in x0 and

A3: Rdiff (f,x0) = Ldiff (f,x0) ; :: thesis: ( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

A4: ex N being Neighbourhood of x0 st N c= dom f

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff (f,x0) = Ldiff (f,x0) implies ( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) ) )

assume that

A1: f is_right_differentiable_in x0 and

A2: f is_left_differentiable_in x0 and

A3: Rdiff (f,x0) = Ldiff (f,x0) ; :: thesis: ( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

A4: ex N being Neighbourhood of x0 st N c= dom f

proof

for h being non-zero 0 -convergent Real_Sequence
consider r2 being Real such that

A5: r2 > 0 and

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

consider r1 being Real such that

A7: r1 > 0 and

A8: [.(x0 - r1),x0.] c= dom f by A2;

set r = min (r1,r2);

min (r1,r2) > 0 by A7, A5, XXREAL_0:15;

then reconsider N = ].(x0 - (min (r1,r2))),(x0 + (min (r1,r2))).[ as Neighbourhood of x0 by RCOMP_1:def 6;

take N ; :: thesis: N c= dom f

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom f )

assume x in N ; :: thesis: x in dom f

then x in { g where g is Real : ( x0 - (min (r1,r2)) < g & g < x0 + (min (r1,r2)) ) } by RCOMP_1:def 2;

then consider g being Real such that

A9: g = x and

A10: x0 - (min (r1,r2)) < g and

A11: g < x0 + (min (r1,r2)) ;

end;A5: r2 > 0 and

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

consider r1 being Real such that

A7: r1 > 0 and

A8: [.(x0 - r1),x0.] c= dom f by A2;

set r = min (r1,r2);

min (r1,r2) > 0 by A7, A5, XXREAL_0:15;

then reconsider N = ].(x0 - (min (r1,r2))),(x0 + (min (r1,r2))).[ as Neighbourhood of x0 by RCOMP_1:def 6;

take N ; :: thesis: N c= dom f

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom f )

assume x in N ; :: thesis: x in dom f

then x in { g where g is Real : ( x0 - (min (r1,r2)) < g & g < x0 + (min (r1,r2)) ) } by RCOMP_1:def 2;

then consider g being Real such that

A9: g = x and

A10: x0 - (min (r1,r2)) < g and

A11: g < x0 + (min (r1,r2)) ;

now :: thesis: x in dom fend;

hence
x in dom f
; :: thesis: verumper cases
( g <= x0 or g > x0 )
;

end;

suppose A12:
g <= x0
; :: thesis: x in dom f

min (r1,r2) <= r1
by XXREAL_0:17;

then x0 - r1 <= x0 - (min (r1,r2)) by XREAL_1:13;

then x0 - r1 <= g by A10, XXREAL_0:2;

then g in { g1 where g1 is Real : ( x0 - r1 <= g1 & g1 <= x0 ) } by A12;

then g in [.(x0 - r1),x0.] by RCOMP_1:def 1;

hence x in dom f by A8, A9; :: thesis: verum

end;then x0 - r1 <= x0 - (min (r1,r2)) by XREAL_1:13;

then x0 - r1 <= g by A10, XXREAL_0:2;

then g in { g1 where g1 is Real : ( x0 - r1 <= g1 & g1 <= x0 ) } by A12;

then g in [.(x0 - r1),x0.] by RCOMP_1:def 1;

hence x in dom f by A8, A9; :: thesis: verum

suppose A13:
g > x0
; :: thesis: x in dom f

min (r1,r2) <= r2
by XXREAL_0:17;

then x0 + (min (r1,r2)) <= x0 + r2 by XREAL_1:7;

then g <= x0 + r2 by A11, XXREAL_0:2;

then g in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r2 ) } by A13;

then g in [.x0,(x0 + r2).] by RCOMP_1:def 1;

hence x in dom f by A6, A9; :: thesis: verum

end;then x0 + (min (r1,r2)) <= x0 + r2 by XREAL_1:7;

then g <= x0 + r2 by A11, XXREAL_0:2;

then g in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r2 ) } by A13;

then g in [.x0,(x0 + r2).] by RCOMP_1:def 1;

hence x in dom f by A6, A9; :: thesis: verum

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

proof

hence
( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )
by A3, A4, FDIFF_2:12; :: thesis: verum
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) ) )

assume that

A14: rng c = {x0} and

A15: rng (h + c) c= dom f ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

A16: rng c c= dom f

end;( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom f implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) ) )

assume that

A14: rng c = {x0} and

A15: rng (h + c) c= dom f ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

A16: rng c c= dom f

proof

consider S being Neighbourhood of x0 such that

A17: S c= dom f by A4;

x0 in S by RCOMP_1:16;

hence rng c c= dom f by A14, A17, ZFMISC_1:31; :: thesis: verum

end;A17: S c= dom f by A4;

x0 in S by RCOMP_1:16;

hence rng c c= dom f by A14, A17, ZFMISC_1:31; :: thesis: verum

now :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )end;

hence
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )
; :: thesis: verumper cases
( ex N being Element of NAT st

for n being Element of NAT st n >= N holds

h . n > 0 or for N being Element of NAT ex n being Element of NAT st

( n >= N & h . n <= 0 ) ) ;

end;

for n being Element of NAT st n >= N holds

h . n > 0 or for N being Element of NAT ex n being Element of NAT st

( n >= N & h . n <= 0 ) ) ;

suppose
ex N being Element of NAT st

for n being Element of NAT st n >= N holds

h . n > 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

for n being Element of NAT st n >= N holds

h . n > 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

then consider N being Element of NAT such that

A18: for n being Element of NAT st n >= N holds

h . n > 0 ;

set h1 = h ^\ N;

A19: for n being Nat holds (h ^\ N) . n > 0

A20: rng (c ^\ N) = {x0}

then A24: ((h ^\ N) ") (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N))) = ((h ^\ N) ") (#) (((f /* (h + c)) ^\ N) - (f /* (c ^\ N))) by A15, VALUED_0:27

.= ((h ^\ N) ") (#) (((f /* (h + c)) ^\ N) - ((f /* c) ^\ N)) by A16, VALUED_0:27

.= ((h ^\ N) ") (#) (((f /* (h + c)) - (f /* c)) ^\ N) by SEQM_3:17

.= ((h ") ^\ N) (#) (((f /* (h + c)) - (f /* c)) ^\ N) by SEQM_3:18

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ N by SEQM_3:19 ;

rng ((h ^\ N) + (c ^\ N)) c= rng (h + c) by A23, VALUED_0:21;

then A25: rng ((h ^\ N) + (c ^\ N)) c= dom f by A15;

then A26: ((h ^\ N) ") (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N))) is convergent by A1, A20, A19;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A24, SEQ_4:21; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0)

lim (((h ^\ N) ") (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N)))) = Rdiff (f,x0) by A1, A20, A25, A19, Th15;

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) by A3, A26, A24, SEQ_4:22; :: thesis: verum

end;A18: for n being Element of NAT st n >= N holds

h . n > 0 ;

set h1 = h ^\ N;

A19: for n being Nat holds (h ^\ N) . n > 0

proof

set c1 = c ^\ N;
let n be Nat; :: thesis: (h ^\ N) . n > 0

( (h ^\ N) . n = h . (n + N) & N + 0 <= n + N ) by NAT_1:def 3, XREAL_1:7;

hence (h ^\ N) . n > 0 by A18; :: thesis: verum

end;( (h ^\ N) . n = h . (n + N) & N + 0 <= n + N ) by NAT_1:def 3, XREAL_1:7;

hence (h ^\ N) . n > 0 by A18; :: thesis: verum

A20: rng (c ^\ N) = {x0}

proof

A23:
(h ^\ N) + (c ^\ N) = (h + c) ^\ N
by SEQM_3:15;
thus
rng (c ^\ N) c= {x0}
by A14, VALUED_0:21; :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng (c ^\ N)

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

A21: c . N in rng c by VALUED_0:28;

assume x in {x0} ; :: thesis: x in rng (c ^\ N)

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

(c ^\ N) . 0 = c . (0 + N) by NAT_1:def 3

.= c . N ;

then (c ^\ N) . 0 = x by A14, A22, A21, TARSKI:def 1;

hence x in rng (c ^\ N) by VALUED_0:28; :: thesis: verum

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

A21: c . N in rng c by VALUED_0:28;

assume x in {x0} ; :: thesis: x in rng (c ^\ N)

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

(c ^\ N) . 0 = c . (0 + N) by NAT_1:def 3

.= c . N ;

then (c ^\ N) . 0 = x by A14, A22, A21, TARSKI:def 1;

hence x in rng (c ^\ N) by VALUED_0:28; :: thesis: verum

then A24: ((h ^\ N) ") (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N))) = ((h ^\ N) ") (#) (((f /* (h + c)) ^\ N) - (f /* (c ^\ N))) by A15, VALUED_0:27

.= ((h ^\ N) ") (#) (((f /* (h + c)) ^\ N) - ((f /* c) ^\ N)) by A16, VALUED_0:27

.= ((h ^\ N) ") (#) (((f /* (h + c)) - (f /* c)) ^\ N) by SEQM_3:17

.= ((h ") ^\ N) (#) (((f /* (h + c)) - (f /* c)) ^\ N) by SEQM_3:18

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ N by SEQM_3:19 ;

rng ((h ^\ N) + (c ^\ N)) c= rng (h + c) by A23, VALUED_0:21;

then A25: rng ((h ^\ N) + (c ^\ N)) c= dom f by A15;

then A26: ((h ^\ N) ") (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N))) is convergent by A1, A20, A19;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A24, SEQ_4:21; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0)

lim (((h ^\ N) ") (#) ((f /* ((h ^\ N) + (c ^\ N))) - (f /* (c ^\ N)))) = Rdiff (f,x0) by A1, A20, A25, A19, Th15;

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) by A3, A26, A24, SEQ_4:22; :: thesis: verum

suppose A27:
for N being Element of NAT ex n being Element of NAT st

( n >= N & h . n <= 0 ) ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

end;

( n >= N & h . n <= 0 ) ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

now :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )end;

hence
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )
; :: thesis: verumper cases
( ex M being Element of NAT st

for m being Element of NAT st m >= M holds

h . m < 0 or for M being Element of NAT ex m being Element of NAT st

( m >= M & h . m >= 0 ) ) ;

end;

for m being Element of NAT st m >= M holds

h . m < 0 or for M being Element of NAT ex m being Element of NAT st

( m >= M & h . m >= 0 ) ) ;

suppose
ex M being Element of NAT st

for m being Element of NAT st m >= M holds

h . m < 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

for m being Element of NAT st m >= M holds

h . m < 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

then consider M being Element of NAT such that

A28: for n being Element of NAT st n >= M holds

h . n < 0 ;

set h1 = h ^\ M;

A29: for n being Nat holds (h ^\ M) . n < 0

A30: rng (c ^\ M) = {x0}

then A34: ((h ^\ M) ") (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M))) = ((h ^\ M) ") (#) (((f /* (h + c)) ^\ M) - (f /* (c ^\ M))) by A15, VALUED_0:27

.= ((h ^\ M) ") (#) (((f /* (h + c)) ^\ M) - ((f /* c) ^\ M)) by A16, VALUED_0:27

.= ((h ^\ M) ") (#) (((f /* (h + c)) - (f /* c)) ^\ M) by SEQM_3:17

.= ((h ") ^\ M) (#) (((f /* (h + c)) - (f /* c)) ^\ M) by SEQM_3:18

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ M by SEQM_3:19 ;

rng ((h ^\ M) + (c ^\ M)) c= rng (h + c) by A33, VALUED_0:21;

then A35: rng ((h ^\ M) + (c ^\ M)) c= dom f by A15;

then A36: ((h ^\ M) ") (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M))) is convergent by A2, A30, A29;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A34, SEQ_4:21; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0)

lim (((h ^\ M) ") (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M)))) = Ldiff (f,x0) by A2, A30, A35, A29, Th9;

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) by A36, A34, SEQ_4:22; :: thesis: verum

end;A28: for n being Element of NAT st n >= M holds

h . n < 0 ;

set h1 = h ^\ M;

A29: for n being Nat holds (h ^\ M) . n < 0

proof

set c1 = c ^\ M;
let n be Nat; :: thesis: (h ^\ M) . n < 0

( (h ^\ M) . n = h . (n + M) & M + 0 <= n + M ) by NAT_1:def 3, XREAL_1:7;

hence (h ^\ M) . n < 0 by A28; :: thesis: verum

end;( (h ^\ M) . n = h . (n + M) & M + 0 <= n + M ) by NAT_1:def 3, XREAL_1:7;

hence (h ^\ M) . n < 0 by A28; :: thesis: verum

A30: rng (c ^\ M) = {x0}

proof

A33:
(h ^\ M) + (c ^\ M) = (h + c) ^\ M
by SEQM_3:15;
thus
rng (c ^\ M) c= {x0}
by A14, VALUED_0:21; :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng (c ^\ M)

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

A31: c . M in rng c by VALUED_0:28;

assume x in {x0} ; :: thesis: x in rng (c ^\ M)

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

(c ^\ M) . 0 = c . (0 + M) by NAT_1:def 3

.= c . M ;

then (c ^\ M) . 0 = x by A14, A32, A31, TARSKI:def 1;

hence x in rng (c ^\ M) by VALUED_0:28; :: thesis: verum

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

A31: c . M in rng c by VALUED_0:28;

assume x in {x0} ; :: thesis: x in rng (c ^\ M)

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

(c ^\ M) . 0 = c . (0 + M) by NAT_1:def 3

.= c . M ;

then (c ^\ M) . 0 = x by A14, A32, A31, TARSKI:def 1;

hence x in rng (c ^\ M) by VALUED_0:28; :: thesis: verum

then A34: ((h ^\ M) ") (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M))) = ((h ^\ M) ") (#) (((f /* (h + c)) ^\ M) - (f /* (c ^\ M))) by A15, VALUED_0:27

.= ((h ^\ M) ") (#) (((f /* (h + c)) ^\ M) - ((f /* c) ^\ M)) by A16, VALUED_0:27

.= ((h ^\ M) ") (#) (((f /* (h + c)) - (f /* c)) ^\ M) by SEQM_3:17

.= ((h ") ^\ M) (#) (((f /* (h + c)) - (f /* c)) ^\ M) by SEQM_3:18

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) ^\ M by SEQM_3:19 ;

rng ((h ^\ M) + (c ^\ M)) c= rng (h + c) by A33, VALUED_0:21;

then A35: rng ((h ^\ M) + (c ^\ M)) c= dom f by A15;

then A36: ((h ^\ M) ") (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M))) is convergent by A2, A30, A29;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A34, SEQ_4:21; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0)

lim (((h ^\ M) ") (#) ((f /* ((h ^\ M) + (c ^\ M))) - (f /* (c ^\ M)))) = Ldiff (f,x0) by A2, A30, A35, A29, Th9;

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) by A36, A34, SEQ_4:22; :: thesis: verum

suppose A37:
for M being Element of NAT ex m being Element of NAT st

( m >= M & h . m >= 0 ) ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

( m >= M & h . m >= 0 ) ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) )

set s = (h ") (#) ((f /* (h + c)) - (f /* c));

defpred S_{1}[ Real] means $1 > 0 ;

defpred S_{2}[ Real] means $1 < 0 ;

A38: for N being Element of NAT ex n being Element of NAT st

( n >= N & S_{2}[h . n] )

A41: ( ( for n being Nat holds S_{2}[(h * q1) . n] ) & ( for n being Element of NAT st ( for r being Real st r = h . n holds

S_{2}[r] ) holds

ex m being Element of NAT st n = q1 . m ) ) from FDIFF_2:sch 1(A38);

A42: for N being Element of NAT ex n being Element of NAT st

( n >= N & S_{1}[h . n] )

A45: ( ( for n being Nat holds S_{1}[(h * q2) . n] ) & ( for n being Element of NAT st ( for r being Real st r = h . n holds

S_{1}[r] ) holds

ex m being Element of NAT st n = q2 . m ) ) from FDIFF_2:sch 1(A42);

set h1 = h * q1;

reconsider h1 = h * q1 as subsequence of h ;

A46: h1 is convergent by SEQ_4:16;

A47: lim h = 0 ;

then A48: lim h1 = 0 by SEQ_4:17;

set h2 = h * q2;

A49: h * q2 is convergent by SEQ_4:16;

lim (h * q2) = 0 by A47, SEQ_4:17;

then reconsider h2 = h * q2 as non-zero 0 -convergent Real_Sequence by A49, FDIFF_1:def 1;

set c2 = c * q2;

A50: rng (c * q2) = {x0} by A14, VALUED_0:26;

reconsider c2 = c * q2 as constant Real_Sequence ;

rng ((h + c) * q2) c= rng (h + c) by VALUED_0:21;

then rng ((h + c) * q2) c= dom f by A15;

then rng (h2 + c2) c= dom f by RFUNCT_2:2;

then A51: ( (h2 ") (#) ((f /* (h2 + c2)) - (f /* c2)) is convergent & lim ((h2 ") (#) ((f /* (h2 + c2)) - (f /* c2))) = Ldiff (f,x0) ) by A1, A3, A45, A50, Th15;

A52: (h2 ") (#) ((f /* (h2 + c2)) - (f /* c2)) = (h2 ") (#) ((f /* ((h + c) * q2)) - (f /* c2)) by RFUNCT_2:2

.= (h2 ") (#) (((f /* (h + c)) * q2) - (f /* c2)) by A15, FUNCT_2:110

.= ((h ") * q2) (#) (((f /* (h + c)) * q2) - (f /* c2)) by RFUNCT_2:5

.= ((h ") * q2) (#) (((f /* (h + c)) * q2) - ((f /* c) * q2)) by A16, FUNCT_2:110

.= ((h ") * q2) (#) (((f /* (h + c)) - (f /* c)) * q2) by RFUNCT_2:2

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) * q2 by RFUNCT_2:2 ;

reconsider h1 = h1 as non-zero 0 -convergent Real_Sequence by A46, A48, FDIFF_1:def 1;

set c1 = c * q1;

A53: rng (c * q1) = {x0} by A14, VALUED_0:26;

reconsider c1 = c * q1 as constant Real_Sequence ;

rng ((h + c) * q1) c= rng (h + c) by VALUED_0:21;

then rng ((h + c) * q1) c= dom f by A15;

then rng (h1 + c1) c= dom f by RFUNCT_2:2;

then A54: ( (h1 ") (#) ((f /* (h1 + c1)) - (f /* c1)) is convergent & lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = Ldiff (f,x0) ) by A2, A41, A53, Th9;

A55: (h1 ") (#) ((f /* (h1 + c1)) - (f /* c1)) = (h1 ") (#) ((f /* ((h + c) * q1)) - (f /* c1)) by RFUNCT_2:2

.= (h1 ") (#) (((f /* (h + c)) * q1) - (f /* c1)) by A15, FUNCT_2:110

.= ((h ") * q1) (#) (((f /* (h + c)) * q1) - (f /* c1)) by RFUNCT_2:5

.= ((h ") * q1) (#) (((f /* (h + c)) * q1) - ((f /* c) * q1)) by A16, FUNCT_2:110

.= ((h ") * q1) (#) (((f /* (h + c)) - (f /* c)) * q1) by RFUNCT_2:2

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) * q1 by RFUNCT_2:2 ;

A56: for g1 being Real st 0 < g1 holds

ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) by A56, SEQ_2:def 7; :: thesis: verum

end;defpred S

defpred S

A38: for N being Element of NAT ex n being Element of NAT st

( n >= N & S

proof

consider q1 being V45() sequence of NAT such that
let m be Element of NAT ; :: thesis: ex n being Element of NAT st

( n >= m & S_{2}[h . n] )

consider n being Element of NAT such that

A39: n >= m and

A40: h . n <= 0 by A27;

take n ; :: thesis: ( n >= m & S_{2}[h . n] )

thus n >= m by A39; :: thesis: S_{2}[h . n]

h . n <> 0 by SEQ_1:5;

hence S_{2}[h . n]
by A40; :: thesis: verum

end;( n >= m & S

consider n being Element of NAT such that

A39: n >= m and

A40: h . n <= 0 by A27;

take n ; :: thesis: ( n >= m & S

thus n >= m by A39; :: thesis: S

h . n <> 0 by SEQ_1:5;

hence S

A41: ( ( for n being Nat holds S

S

ex m being Element of NAT st n = q1 . m ) ) from FDIFF_2:sch 1(A38);

A42: for N being Element of NAT ex n being Element of NAT st

( n >= N & S

proof

consider q2 being V45() sequence of NAT such that
let m be Element of NAT ; :: thesis: ex n being Element of NAT st

( n >= m & S_{1}[h . n] )

consider n being Element of NAT such that

A43: n >= m and

A44: h . n >= 0 by A37;

take n ; :: thesis: ( n >= m & S_{1}[h . n] )

thus n >= m by A43; :: thesis: S_{1}[h . n]

h . n <> 0 by SEQ_1:5;

hence S_{1}[h . n]
by A44; :: thesis: verum

end;( n >= m & S

consider n being Element of NAT such that

A43: n >= m and

A44: h . n >= 0 by A37;

take n ; :: thesis: ( n >= m & S

thus n >= m by A43; :: thesis: S

h . n <> 0 by SEQ_1:5;

hence S

A45: ( ( for n being Nat holds S

S

ex m being Element of NAT st n = q2 . m ) ) from FDIFF_2:sch 1(A42);

set h1 = h * q1;

reconsider h1 = h * q1 as subsequence of h ;

A46: h1 is convergent by SEQ_4:16;

A47: lim h = 0 ;

then A48: lim h1 = 0 by SEQ_4:17;

set h2 = h * q2;

A49: h * q2 is convergent by SEQ_4:16;

lim (h * q2) = 0 by A47, SEQ_4:17;

then reconsider h2 = h * q2 as non-zero 0 -convergent Real_Sequence by A49, FDIFF_1:def 1;

set c2 = c * q2;

A50: rng (c * q2) = {x0} by A14, VALUED_0:26;

reconsider c2 = c * q2 as constant Real_Sequence ;

rng ((h + c) * q2) c= rng (h + c) by VALUED_0:21;

then rng ((h + c) * q2) c= dom f by A15;

then rng (h2 + c2) c= dom f by RFUNCT_2:2;

then A51: ( (h2 ") (#) ((f /* (h2 + c2)) - (f /* c2)) is convergent & lim ((h2 ") (#) ((f /* (h2 + c2)) - (f /* c2))) = Ldiff (f,x0) ) by A1, A3, A45, A50, Th15;

A52: (h2 ") (#) ((f /* (h2 + c2)) - (f /* c2)) = (h2 ") (#) ((f /* ((h + c) * q2)) - (f /* c2)) by RFUNCT_2:2

.= (h2 ") (#) (((f /* (h + c)) * q2) - (f /* c2)) by A15, FUNCT_2:110

.= ((h ") * q2) (#) (((f /* (h + c)) * q2) - (f /* c2)) by RFUNCT_2:5

.= ((h ") * q2) (#) (((f /* (h + c)) * q2) - ((f /* c) * q2)) by A16, FUNCT_2:110

.= ((h ") * q2) (#) (((f /* (h + c)) - (f /* c)) * q2) by RFUNCT_2:2

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) * q2 by RFUNCT_2:2 ;

reconsider h1 = h1 as non-zero 0 -convergent Real_Sequence by A46, A48, FDIFF_1:def 1;

set c1 = c * q1;

A53: rng (c * q1) = {x0} by A14, VALUED_0:26;

reconsider c1 = c * q1 as constant Real_Sequence ;

rng ((h + c) * q1) c= rng (h + c) by VALUED_0:21;

then rng ((h + c) * q1) c= dom f by A15;

then rng (h1 + c1) c= dom f by RFUNCT_2:2;

then A54: ( (h1 ") (#) ((f /* (h1 + c1)) - (f /* c1)) is convergent & lim ((h1 ") (#) ((f /* (h1 + c1)) - (f /* c1))) = Ldiff (f,x0) ) by A2, A41, A53, Th9;

A55: (h1 ") (#) ((f /* (h1 + c1)) - (f /* c1)) = (h1 ") (#) ((f /* ((h + c) * q1)) - (f /* c1)) by RFUNCT_2:2

.= (h1 ") (#) (((f /* (h + c)) * q1) - (f /* c1)) by A15, FUNCT_2:110

.= ((h ") * q1) (#) (((f /* (h + c)) * q1) - (f /* c1)) by RFUNCT_2:5

.= ((h ") * q1) (#) (((f /* (h + c)) * q1) - ((f /* c) * q1)) by A16, FUNCT_2:110

.= ((h ") * q1) (#) (((f /* (h + c)) - (f /* c)) * q1) by RFUNCT_2:2

.= ((h ") (#) ((f /* (h + c)) - (f /* c))) * q1 by RFUNCT_2:2 ;

A56: for g1 being Real st 0 < g1 holds

ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

proof

hence
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0)
let g1 be Real; :: thesis: ( 0 < g1 implies ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 )

assume A57: 0 < g1 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

then consider n1 being Nat such that

A58: for m being Nat st n1 <= m holds

|.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q1) . m) - (Ldiff (f,x0))).| < g1 by A54, A55, SEQ_2:def 7;

consider n2 being Nat such that

A59: for m being Nat st n2 <= m holds

|.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q2) . m) - (Ldiff (f,x0))).| < g1 by A51, A52, A57, SEQ_2:def 7;

take n = max ((q1 . n1),(q2 . n2)); :: thesis: for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 )

assume A60: n <= m ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

A61: m in NAT by ORDINAL1:def 12;

A62: n >= q2 . n2 by XXREAL_0:25;

A63: n >= q1 . n1 by XXREAL_0:25;

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

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 )

assume A57: 0 < g1 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

then consider n1 being Nat such that

A58: for m being Nat st n1 <= m holds

|.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q1) . m) - (Ldiff (f,x0))).| < g1 by A54, A55, SEQ_2:def 7;

consider n2 being Nat such that

A59: for m being Nat st n2 <= m holds

|.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q2) . m) - (Ldiff (f,x0))).| < g1 by A51, A52, A57, SEQ_2:def 7;

take n = max ((q1 . n1),(q2 . n2)); :: thesis: for m being Nat st n <= m holds

|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 )

assume A60: n <= m ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

A61: m in NAT by ORDINAL1:def 12;

A62: n >= q2 . n2 by XXREAL_0:25;

A63: n >= q1 . n1 by XXREAL_0:25;

per cases
( h . m > 0 or h . m <= 0 )
;

end;

suppose
h . m > 0
; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

then
for r being Real st r = h . m holds

r > 0 ;

then consider k being Element of NAT such that

A64: m = q2 . k by A45, A61;

A65: n2 in NAT by ORDINAL1:def 12;

( dom q2 = NAT & q2 . k >= q2 . n2 ) by A60, A62, A64, FUNCT_2:def 1, XXREAL_0:2;

then not k < n2 by VALUED_0:def 13, A65;

then |.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q2) . k) - (Ldiff (f,x0))).| < g1 by A59;

hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 by A64, FUNCT_2:15; :: thesis: verum

end;r > 0 ;

then consider k being Element of NAT such that

A64: m = q2 . k by A45, A61;

A65: n2 in NAT by ORDINAL1:def 12;

( dom q2 = NAT & q2 . k >= q2 . n2 ) by A60, A62, A64, FUNCT_2:def 1, XXREAL_0:2;

then not k < n2 by VALUED_0:def 13, A65;

then |.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q2) . k) - (Ldiff (f,x0))).| < g1 by A59;

hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 by A64, FUNCT_2:15; :: thesis: verum

suppose A66:
h . m <= 0
; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1

h . m <> 0
by SEQ_1:5;

then for r being Real st r = h . m holds

r < 0 by A66;

then consider k being Element of NAT such that

A67: m = q1 . k by A41, A61;

A68: n1 in NAT by ORDINAL1:def 12;

( dom q1 = NAT & q1 . k >= q1 . n1 ) by A60, A63, A67, FUNCT_2:def 1, XXREAL_0:2;

then not k < n1 by VALUED_0:def 13, A68;

then |.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q1) . k) - (Ldiff (f,x0))).| < g1 by A58;

hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 by A67, FUNCT_2:15; :: thesis: verum

end;then for r being Real st r = h . m holds

r < 0 by A66;

then consider k being Element of NAT such that

A67: m = q1 . k by A41, A61;

A68: n1 in NAT by ORDINAL1:def 12;

( dom q1 = NAT & q1 . k >= q1 . n1 ) by A60, A63, A67, FUNCT_2:def 1, XXREAL_0:2;

then not k < n1 by VALUED_0:def 13, A68;

then |.(((((h ") (#) ((f /* (h + c)) - (f /* c))) * q1) . k) - (Ldiff (f,x0))).| < g1 by A58;

hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (Ldiff (f,x0))).| < g1 by A67, FUNCT_2:15; :: thesis: verum

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Ldiff (f,x0) by A56, SEQ_2:def 7; :: thesis: verum