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

proof

assume not [.(x0 - (min r0,r2)),x0.] c= dom (f ^ ) ; :: thesis: contradiction
then consider x being set such that
A16: ( x in [.(x0 - (min r0,r2)),x0.] & not x in dom (f ^ ) ) by TARSKI:def 3;
reconsider x = x as Real by A16;
A17: not x in (dom f) \ (f " {0 }) by A16, RFUNCT_1:def 8;

now

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 A14, A16; :: thesis: verum

end;

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

then ( x in dom f & f . x in {0 } ) by FUNCT_1:def 13;
then ( x in dom f & f . x = 0 ) by TARSKI:def 1;
hence contradiction by A2, A10, A16; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f ^ ) & ( for n being Element of NAT holds h . n < 0 ) holds
( (h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)) is convergent & lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) = - ((Ldiff f,x0) / ((f . x0) ^2 )) )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f ^ ) & ( for n being Element of NAT holds h . n < 0 ) holds
( (h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)) is convergent & lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) = - ((Ldiff f,x0) / ((f . x0) ^2 )) )
let c be V6 Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f ^ ) & ( for n being Element of NAT holds h . n < 0 ) implies ( (h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)) is convergent & lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) = - ((Ldiff f,x0) / ((f . x0) ^2 )) ) )
assume that
A18: rng c = {x0} and
A19: rng (h + c) c= dom (f ^ ) and
A20: for n being Element of NAT holds h . n < 0 ; :: thesis: ( (h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)) is convergent & lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) = - ((Ldiff f,x0) / ((f . x0) ^2 )) )
A21: rng (h + c) c= (dom f) \ (f " {0 }) by A19, RFUNCT_1:def 8;
A22: ( h is convergent & lim h = 0 & h is non-zero ) by FDIFF_1:def 1;
(dom f) \ (f " {0 }) c= dom f by XBOOLE_1:36;
then A23: rng (h + c) c= dom f by A21, XBOOLE_1:1;
Ldiff f,x0 = Ldiff f,x0 ;
then A24: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = Ldiff f,x0 ) by A1, A18, A20, A23, Th9;
A25: f /* (h + c) is non-zero by A19, RFUNCT_2:26;
A26: 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 A18, TARSKI:def 1; :: thesis: verum

end;

x0 in dom (f ^ ) by A6, A15;
then A27: x0 in (dom f) \ (f " {0 }) by RFUNCT_1:def 8;
rng c c= (dom f) \ (f " {0 })

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in (dom f) \ (f " {0 }) )
assume x in rng c ; :: thesis: x in (dom f) \ (f " {0 })
hence x in (dom f) \ (f " {0 }) by A18, A27, TARSKI:def 1; :: thesis: verum

end;

then A28: rng c c= dom (f ^ ) by RFUNCT_1:def 8;
then A29: f /* c is non-zero by RFUNCT_2:26;
then A30: (f /* (h + c)) (#) (f /* c) is non-zero by A25, SEQ_1:43;
dom (f ^ ) = (dom f) \ (f " {0 }) by RFUNCT_1:def 8;
then A31: dom (f ^ ) c= dom f by XBOOLE_1:36;
A32: for g being real number st 0 < g holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g

proof

let g be real number ; :: thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g )
assume A33: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f /* c) . m) - (f . x0)) < g )
assume n <= m ; :: thesis: abs (((f /* c) . m) - (f . x0)) < g
abs (((f /* c) . m) - (f . x0)) = abs ((f . (c . m)) - (f . x0)) by A28, A31, FUNCT_2:185, XBOOLE_1:1
.= abs ((f . x0) - (f . x0)) by A26
.= 0 by ABSVALUE:def 1 ;
hence abs (((f /* c) . m) - (f . x0)) < g by A33; :: thesis: verum

end;

then A34: f /* c is convergent by SEQ_2:def 6;
then A35: lim (f /* c) = f . x0 by A32, SEQ_2:def 7;
A36: h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A22, A24, SEQ_2:28;
A37: h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c)

proof

now

let n be Element of NAT ; :: thesis: (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A38: h . n <> 0 by A20;
thus (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) . n = ((h (#) (h " )) (#) ((f /* (h + c)) - (f /* c))) . n by SEQ_1:22
.= ((h (#) (h " )) . n) * (((f /* (h + c)) - (f /* c)) . n) by SEQ_1:12
.= ((h . n) * ((h " ) . n)) * (((f /* (h + c)) - (f /* c)) . n) by SEQ_1:12
.= ((h . n) * ((h . n) " )) * (((f /* (h + c)) - (f /* c)) . n) by VALUED_1:10
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A38, XCMPLX_0:def 7
.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum

end;

hence h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:113; :: thesis: verum

end;

(f /* c) + ((f /* (h + c)) - (f /* c)) = f /* (h + c)

proof

now

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:11
.= ((f /* c) . n) + (((f /* (h + c)) . n) - ((f /* c) . n)) by RFUNCT_2:6
.= (f /* (h + c)) . n ; :: thesis: verum

end;

hence (f /* c) + ((f /* (h + c)) - (f /* c)) = f /* (h + c) by FUNCT_2:113; :: thesis: verum

end;

then A39: f /* (h + c) is convergent by A34, A36, A37, SEQ_2:19;
lim (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = (lim h) * (lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A22, A24, SEQ_2:29
.= 0 by A22 ;
then A40: 0 = (lim (f /* (h + c))) - (f . x0) by A34, A35, A37, A39, SEQ_2:26;
A41: (f /* (h + c)) (#) (f /* c) is convergent by A34, A39, SEQ_2:28;
A42: lim ((f /* (h + c)) (#) (f /* c)) = (f . x0) ^2 by A34, A35, A39, A40, SEQ_2:29;
A43: lim ((f /* (h + c)) (#) (f /* c)) <> 0

proof

assume not lim ((f /* (h + c)) (#) (f /* c)) <> 0 ; :: thesis: contradiction
then f . x0 = 0 by A42, XCMPLX_1:6;
hence contradiction by A2, A3, A9, A13; :: thesis: verum

end;

A44: - ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A24, SEQ_2:23;

now

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
A45: (f /* (h + c)) . n <> 0 by A25, SEQ_1:7;
A46: (f /* c) . n <> 0 by A29, SEQ_1:7;
thus ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) . n = ((h " ) . n) * ((((f ^ ) /* (h + c)) - ((f ^ ) /* c)) . n) by SEQ_1:12
.= ((h " ) . n) * ((((f ^ ) /* (h + c)) . n) - (((f ^ ) /* c) . n)) by RFUNCT_2:6
.= ((h " ) . n) * ((((f /* (h + c)) " ) . n) - (((f ^ ) /* c) . n)) by A19, RFUNCT_2:27
.= ((h " ) . n) * ((((f /* (h + c)) " ) . n) - (((f /* c) " ) . n)) by A28, RFUNCT_2:27
.= ((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:217
.= ((h " ) . n) * ((1 / ((f /* (h + c)) . n)) - (1 / ((f /* c) . n))) by XCMPLX_1:217
.= ((h " ) . n) * (((1 * ((f /* c) . n)) - (1 * ((f /* (h + c)) . n))) / (((f /* (h + c)) . n) * ((f /* c) . n))) by A45, A46, XCMPLX_1:131
.= ((h " ) . n) * ((- (((f /* (h + c)) . n) - ((f /* c) . n))) / (((f /* (h + c)) (#) (f /* c)) . n)) by SEQ_1:12
.= ((h " ) . n) * ((- (((f /* (h + c)) - (f /* c)) . n)) / (((f /* (h + c)) (#) (f /* c)) . n)) by RFUNCT_2:6
.= ((h " ) . n) * (- ((((f /* (h + c)) - (f /* c)) . n) / (((f /* (h + c)) (#) (f /* c)) . n))) by XCMPLX_1:188
.= - (((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:75
.= - ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . n) / (((f /* (h + c)) (#) (f /* c)) . n)) by SEQ_1:12
.= - ((((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:12
.= (- (((h " ) (#) ((f /* (h + c)) - (f /* c))) /" ((f /* (h + c)) (#) (f /* c)))) . n by SEQ_1:14
.= ((- ((h " ) (#) ((f /* (h + c)) - (f /* c)))) /" ((f /* (h + c)) (#) (f /* c))) . n by SEQ_1:56 ; :: thesis: verum

end;

then A47: (h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)) = (- ((h " ) (#) ((f /* (h + c)) - (f /* c)))) /" ((f /* (h + c)) (#) (f /* c)) by FUNCT_2:113;
then lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) = (lim (- ((h " ) (#) ((f /* (h + c)) - (f /* c))))) / ((f . x0) ^2 ) by A30, A41, A42, A43, A44, SEQ_2:38
.= (- (Ldiff f,x0)) / ((f . x0) ^2 ) by A24, SEQ_2:24
.= - ((Ldiff f,x0) / ((f . x0) ^2 )) by XCMPLX_1:188 ;
hence ( (h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)) is convergent & lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) = - ((Ldiff f,x0) / ((f . x0) ^2 )) ) by A30, A41, A43, A44, A47, SEQ_2:37; :: thesis: verum

end;

hence ( f ^ is_left_differentiable_in x0 & Ldiff (f ^ ),x0 = - ((Ldiff f,x0) / ((f . x0) ^2 )) ) by A4, A15, Th9; :: thesis: verum