let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds
f . g <> 0 ) ) holds
( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds
f . g <> 0 ) ) implies ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) )
A1: 0 + x0 = x0 ;
assume A2: f is_right_differentiable_in x0 ; :: thesis: ( for r0 being Real holds
( not r0 > 0 or ex g being Real st
( g in dom f & g in [.x0,(x0 + r0).] & not f . g <> 0 ) ) or ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) )
then consider r2 being Real such that
A3: 0 < r2 and
A4: [.x0,(x0 + r2).] c= dom f ;
given r0 being Real such that A5: r0 > 0 and
A6: for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds
f . g <> 0 ; :: thesis: ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
set r3 = min (r0,r2);
0 <= min (r0,r2) by A5, A3, XXREAL_0:15;
then A7: x0 <= x0 + (min (r0,r2)) by A1, XREAL_1:6;
min (r0,r2) <= r2 by XXREAL_0:17;
then A8: x0 + (min (r0,r2)) <= x0 + r2 by XREAL_1:7;
then x0 <= x0 + r2 by A7, XXREAL_0:2;
then A9: x0 in [.x0,(x0 + r2).] by XXREAL_1:1;
x0 + (min (r0,r2)) in { g where g is Real : ( x0 <= g & g <= x0 + r2 ) } by A7, A8;
then x0 + (min (r0,r2)) in [.x0,(x0 + r2).] by RCOMP_1:def 1;
then [.x0,(x0 + (min (r0,r2))).] c= [.x0,(x0 + r2).] by A9, XXREAL_2:def 12;
then A10: [.x0,(x0 + (min (r0,r2))).] c= dom f by A4;
min (r0,r2) <= r0 by XXREAL_0:17;
then A11: x0 + (min (r0,r2)) <= x0 + r0 by XREAL_1:7;
then x0 <= x0 + r0 by A7, XXREAL_0:2;
then A12: x0 in [.x0,(x0 + r0).] by XXREAL_1:1;
x0 + (min (r0,r2)) in { g where g is Real : ( x0 <= g & g <= x0 + r0 ) } by A7, A11;
then x0 + (min (r0,r2)) in [.x0,(x0 + r0).] by RCOMP_1:def 1;
then A13: [.x0,(x0 + (min (r0,r2))).] c= [.x0,(x0 + r0).] by A12, XXREAL_2:def 12;
A14: [.x0,(x0 + (min (r0,r2))).] c= dom (f ^)

proof

assume not [.x0,(x0 + (min (r0,r2))).] c= dom (f ^) ; :: thesis: contradiction
then consider x being object such that
A15: x in [.x0,(x0 + (min (r0,r2))).] and
A16: not x in dom (f ^) ;
reconsider x = x as Real by A15;
A17: not x in (dom f) \ (f " {0}) by A16, RFUNCT_1:def 2;

now :: thesis: contradiction

per cases ( not x in dom f or x in f " {0} ) by A17, XBOOLE_0:def 5;

suppose not x in dom f ; :: thesis: contradiction

hence contradiction by A10, A15; :: thesis: verum

end;

suppose A18: x in f " {0} ; :: thesis: contradiction

then f . x in {0} by FUNCT_1:def 7;
then A19: f . x = 0 by TARSKI:def 1;
x in dom f by A18, FUNCT_1:def 7;
hence contradiction by A6, A13, A15, A19; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A20: x0 in [.x0,(x0 + (min (r0,r2))).] by A7, XXREAL_1:1;
A21: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f ^) & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )

proof

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 ^) & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f ^) & ( for n being Nat holds h . n > 0 ) implies ( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) )
assume that
A22: rng c = {x0} and
A23: rng (h + c) c= dom (f ^) and
A24: for n being Nat holds h . n > 0 ; :: thesis: ( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
A25: for m being Element of NAT holds c . m = x0

proof

let m be Element of NAT ; :: thesis: c . m = x0
c . m in rng c by VALUED_0:28;
hence c . m = x0 by A22, TARSKI:def 1; :: thesis: verum

end;

A26: (dom f) \ (f " {0}) c= dom f by XBOOLE_1:36;
rng (h + c) c= (dom f) \ (f " {0}) by A23, RFUNCT_1:def 2;
then A27: rng (h + c) c= dom f by A26;
then A28: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = Rdiff (f,x0) by A2, A22, A24, Th15;
A29: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A2, A22, A24, A27;
then A30: - ((h ") (#) ((f /* (h + c)) - (f /* c))) is convergent ;
x0 in dom (f ^) by A20, A14;
then A31: x0 in (dom f) \ (f " {0}) by RFUNCT_1:def 2;
rng c c= (dom f) \ (f " {0}) by A22, A31, TARSKI:def 1;
then A32: rng c c= dom (f ^) by RFUNCT_1:def 2;
then A33: f /* c is non-zero by RFUNCT_2:11;

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

let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A34: h . n <> 0 by A24;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((h (#) (h ")) (#) ((f /* (h + c)) - (f /* c))) . n by SEQ_1:14
.= ((h (#) (h ")) . n) * (((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
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A34, XCMPLX_0:def 7
.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum

end;

then A35: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
A36: f /* (h + c) is non-zero by A23, RFUNCT_2:11;
then A37: (f /* (h + c)) (#) (f /* c) is non-zero by A33, SEQ_1:35;

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

let n be Element of NAT ; :: thesis: ((f /* c) + ((f /* (h + c)) - (f /* c))) . n = (f /* (h + c)) . n
thus ((f /* c) + ((f /* (h + c)) - (f /* c))) . n = ((f /* c) . n) + (((f /* (h + c)) - (f /* c)) . n) by SEQ_1:7
.= ((f /* c) . n) + (((f /* (h + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= (f /* (h + c)) . n ; :: thesis: verum

end;

then A38: (f /* c) + ((f /* (h + c)) - (f /* c)) = f /* (h + c) by FUNCT_2:63;
dom (f ^) = (dom f) \ (f " {0}) by RFUNCT_1:def 2;
then A39: dom (f ^) c= dom f by XBOOLE_1:36;
A40: 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

proof

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 A41: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f /* c) . m) - (f . x0)).| < g
take n = 0 ; :: 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
A42: m in NAT by ORDINAL1:def 12;
|.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by A32, A39, FUNCT_2:108, XBOOLE_1:1, A42
.= |.((f . x0) - (f . x0)).| by A25, A42
.= 0 by ABSVALUE:def 1 ;
hence |.(((f /* c) . m) - (f . x0)).| < g by A41; :: thesis: verum

end;

then A43: f /* c is convergent by SEQ_2:def 6;
then A44: lim (f /* c) = f . x0 by A40, SEQ_2:def 7;
h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) is convergent by A29;
then A45: f /* (h + c) is convergent by A43, A35, A38;
lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = (lim h) * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A29, SEQ_2:15
.= 0 ;
then 0 = (lim (f /* (h + c))) - (f . x0) by A43, A44, A35, A45, SEQ_2:12;
then A46: lim ((f /* (h + c)) (#) (f /* c)) = (f . x0) ^2 by A43, A44, A45, SEQ_2:15;
A47: lim ((f /* (h + c)) (#) (f /* c)) <> 0

proof

assume not lim ((f /* (h + c)) (#) (f /* c)) <> 0 ; :: thesis: contradiction
then f . x0 = 0 by A46, XCMPLX_1:6;
hence contradiction by A6, A4, A12, A9; :: thesis: verum

end;

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

let n be Element of NAT ; :: thesis: ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) . n = ((- ((h ") (#) ((f /* (h + c)) - (f /* c)))) /" ((f /* (h + c)) (#) (f /* c))) . n
A48: ( (f /* (h + c)) . n <> 0 & (f /* c) . n <> 0 ) by A36, A33, SEQ_1:5;
thus ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) . n = ((h ") . n) * ((((f ^) /* (h + c)) - ((f ^) /* c)) . n) by SEQ_1:8
.= ((h ") . n) * ((((f ^) /* (h + c)) . n) - (((f ^) /* c) . n)) by RFUNCT_2:1
.= ((h ") . n) * ((((f /* (h + c)) ") . n) - (((f ^) /* c) . n)) by A23, RFUNCT_2:12
.= ((h ") . n) * ((((f /* (h + c)) ") . n) - (((f /* c) ") . n)) by A32, RFUNCT_2:12
.= ((h ") . n) * ((((f /* (h + c)) . n) ") - (((f /* c) ") . n)) by VALUED_1:10
.= ((h ") . n) * ((((f /* (h + c)) . n) ") - (((f /* c) . n) ")) by VALUED_1:10
.= ((h ") . n) * ((1 / ((f /* (h + c)) . n)) - (((f /* c) . n) ")) by XCMPLX_1:215
.= ((h ") . n) * ((1 / ((f /* (h + c)) . n)) - (1 / ((f /* c) . n))) by XCMPLX_1:215
.= ((h ") . n) * (((1 * ((f /* c) . n)) - (1 * ((f /* (h + c)) . n))) / (((f /* (h + c)) . n) * ((f /* c) . n))) by A48, XCMPLX_1:130
.= ((h ") . n) * ((- (((f /* (h + c)) . n) - ((f /* c) . n))) / (((f /* (h + c)) (#) (f /* c)) . n)) by SEQ_1:8
.= ((h ") . n) * ((- (((f /* (h + c)) - (f /* c)) . n)) / (((f /* (h + c)) (#) (f /* c)) . n)) by RFUNCT_2:1
.= ((h ") . n) * (- ((((f /* (h + c)) - (f /* c)) . n) / (((f /* (h + c)) (#) (f /* c)) . n))) by XCMPLX_1:187
.= - (((h ") . n) * ((((f /* (h + c)) - (f /* c)) . n) / (((f /* (h + c)) (#) (f /* c)) . n)))
.= - ((((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) / (((f /* (h + c)) (#) (f /* c)) . n)) by XCMPLX_1:74
.= - ((((h ") (#) ((f /* (h + c)) - (f /* c))) . n) / (((f /* (h + c)) (#) (f /* c)) . n)) by SEQ_1:8
.= - ((((h ") (#) ((f /* (h + c)) - (f /* c))) . n) * ((((f /* (h + c)) (#) (f /* c)) . n) ")) by XCMPLX_0:def 9
.= - ((((h ") (#) ((f /* (h + c)) - (f /* c))) . n) * ((((f /* (h + c)) (#) (f /* c)) ") . n)) by VALUED_1:10
.= - ((((h ") (#) ((f /* (h + c)) - (f /* c))) /" ((f /* (h + c)) (#) (f /* c))) . n) by SEQ_1:8
.= (- (((h ") (#) ((f /* (h + c)) - (f /* c))) /" ((f /* (h + c)) (#) (f /* c)))) . n by SEQ_1:10
.= ((- ((h ") (#) ((f /* (h + c)) - (f /* c)))) /" ((f /* (h + c)) (#) (f /* c))) . n by SEQ_1:48 ; :: thesis: verum

end;

then A49: (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) = (- ((h ") (#) ((f /* (h + c)) - (f /* c)))) /" ((f /* (h + c)) (#) (f /* c)) by FUNCT_2:63;
A50: (f /* (h + c)) (#) (f /* c) is convergent by A43, A45;
then lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = (lim (- ((h ") (#) ((f /* (h + c)) - (f /* c))))) / ((f . x0) ^2) by A37, A46, A47, A30, A49, SEQ_2:24
.= (- (Rdiff (f,x0))) / ((f . x0) ^2) by A29, A28, SEQ_2:10
.= - ((Rdiff (f,x0)) / ((f . x0) ^2)) by XCMPLX_1:187 ;
hence ( (h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c)) is convergent & lim ((h ") (#) (((f ^) /* (h + c)) - ((f ^) /* c))) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) by A37, A50, A47, A30, A49, SEQ_2:23; :: thesis: verum

end;

0 < min (r0,r2) by A5, A3, XXREAL_0:15;
hence ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) by A14, A21, Th15; :: thesis: verum