let f1, f2 be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds
f2 . g <> 0 ) ) holds
( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
let x0 be Real; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & ex r0 being Real st
( r0 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds
f2 . g <> 0 ) ) implies ( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) )
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0 ; :: thesis: ( for r0 being Real holds
( not r0 > 0 or ex g being Real st
( g in dom f2 & g in [.(x0 - r0),x0.] & not f2 . g <> 0 ) ) or ( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) )
consider r1 being Real such that
A3: 0 < r1 and
A4: [.(x0 - r1),x0.] c= dom f1 by A1, Def4;
given r0 being Real such that A5: r0 > 0 and
A6: for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds
f2 . g <> 0 ; :: thesis: ( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
consider r2 being Real such that
A7: 0 < r2 and
A8: [.(x0 - r2),x0.] c= dom f2 by A2, Def4;
set r3 = min (r0,r2);
A9: 0 < min (r0,r2) by A5, A7, XXREAL_0:15;
then A10: x0 - (min (r0,r2)) <= x0 by XREAL_1:43;
min (r0,r2) <= r2 by XXREAL_0:17;
then A11: x0 - r2 <= x0 - (min (r0,r2)) by XREAL_1:13;
then x0 - r2 <= x0 by A10, XXREAL_0:2;
then A12: x0 in [.(x0 - r2),x0.] by XXREAL_1:1;
x0 - (min (r0,r2)) in { g where g is Real : ( x0 - r2 <= g & g <= x0 ) } by A10, A11;
then x0 - (min (r0,r2)) in [.(x0 - r2),x0.] by RCOMP_1:def 1;
then [.(x0 - (min (r0,r2))),x0.] c= [.(x0 - r2),x0.] by A12, XXREAL_2:def 12;
then A13: [.(x0 - (min (r0,r2))),x0.] c= dom f2 by A8, XBOOLE_1:1;
min (r0,r2) <= r0 by XXREAL_0:17;
then A14: x0 - r0 <= x0 - (min (r0,r2)) by XREAL_1:13;
then x0 - r0 <= x0 by A10, XXREAL_0:2;
then A15: x0 in [.(x0 - r0),x0.] by XXREAL_1:1;
x0 - (min (r0,r2)) in { g where g is Real : ( x0 - r0 <= g & g <= x0 ) } by A10, A14;
then x0 - (min (r0,r2)) in [.(x0 - r0),x0.] by RCOMP_1:def 1;
then A16: [.(x0 - (min (r0,r2))),x0.] c= [.(x0 - r0),x0.] by A15, XXREAL_2:def 12;
set r = min (r1,(min (r0,r2)));
A17: 0 < min (r1,(min (r0,r2))) by A3, A9, XXREAL_0:15;
then A18: x0 - (min (r1,(min (r0,r2)))) <= x0 by XREAL_1:43;
min (r1,(min (r0,r2))) <= min (r0,r2) by XXREAL_0:17;
then A19: x0 - (min (r0,r2)) <= x0 - (min (r1,(min (r0,r2)))) by XREAL_1:13;
then x0 - (min (r0,r2)) <= x0 by A18, XXREAL_0:2;
then A20: x0 in [.(x0 - (min (r0,r2))),x0.] by XXREAL_1:1;
x0 - (min (r1,(min (r0,r2)))) in { g where g is Real : ( x0 - (min (r0,r2)) <= g & g <= x0 ) } by A18, A19;
then x0 - (min (r1,(min (r0,r2)))) in [.(x0 - (min (r0,r2))),x0.] by RCOMP_1:def 1;
then A21: [.(x0 - (min (r1,(min (r0,r2))))),x0.] c= [.(x0 - (min (r0,r2))),x0.] by A20, XXREAL_2:def 12;
[.(x0 - (min (r1,(min (r0,r2))))),x0.] c= dom (f2 ^)

proof

assume not [.(x0 - (min (r1,(min (r0,r2))))),x0.] c= dom (f2 ^) ; :: thesis: contradiction
then consider x being set such that
A22: x in [.(x0 - (min (r1,(min (r0,r2))))),x0.] and
A23: not x in dom (f2 ^) by TARSKI:def 3;
reconsider x = x as Real by A22;
A24: x in [.(x0 - (min (r0,r2))),x0.] by A21, A22;
A25: not x in (dom f2) \ (f2 " {0}) by A23, RFUNCT_1:def 2;

now

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

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

hence contradiction by A13, A24; :: thesis: verum

end;

suppose A26: x in f2 " {0} ; :: thesis: contradiction

then f2 . x in {0} by FUNCT_1:def 7;
then A27: f2 . x = 0 by TARSKI:def 1;
x in dom f2 by A26, FUNCT_1:def 7;
hence contradiction by A6, A16, A24, A27; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then A28: [.(x0 - (min (r1,(min (r0,r2))))),x0.] c= (dom f2) \ (f2 " {0}) by RFUNCT_1:def 2;
min (r1,(min (r0,r2))) <= r1 by XXREAL_0:17;
then A29: x0 - r1 <= x0 - (min (r1,(min (r0,r2)))) by XREAL_1:13;
then x0 - r1 <= x0 by A18, XXREAL_0:2;
then A30: x0 in [.(x0 - r1),x0.] by XXREAL_1:1;
x0 - (min (r1,(min (r0,r2)))) in { g where g is Real : ( x0 - r1 <= g & g <= x0 ) } by A18, A29;
then x0 - (min (r1,(min (r0,r2)))) in [.(x0 - r1),x0.] by RCOMP_1:def 1;
then [.(x0 - (min (r1,(min (r0,r2))))),x0.] c= [.(x0 - r1),x0.] by A30, XXREAL_2:def 12;
then A31: [.(x0 - (min (r1,(min (r0,r2))))),x0.] c= dom f1 by A4, XBOOLE_1:1;
A32: for h being convergent_to_0 Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 / f2) & ( for n being Element of NAT holds h . n < 0 ) holds
( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 / f2) & ( for n being Element of NAT holds h . n < 0 ) holds
( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f1 / f2) & ( for n being Element of NAT holds h . n < 0 ) implies ( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) )
assume that
A33: rng c = {x0} and
A34: rng (h + c) c= dom (f1 / f2) and
A35: for n being Element of NAT holds h . n < 0 ; :: thesis: ( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )
A36: rng (h + c) c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A34, RFUNCT_1:def 1;
0 <= min (r1,(min (r0,r2))) by A3, A9, XXREAL_0:15;
then x0 - (min (r1,(min (r0,r2)))) <= x0 by XREAL_1:43;
then A37: x0 in [.(x0 - (min (r1,(min (r0,r2))))),x0.] by XXREAL_1:1;
then A38: x0 in dom f1 by A31;
A39: rng c c= dom f1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom f1 )
assume x in rng c ; :: thesis: x in dom f1
hence x in dom f1 by A33, A38, TARSKI:def 1; :: thesis: verum

end;

(dom f1) /\ ((dom f2) \ (f2 " {0})) c= dom f1 by XBOOLE_1:17;
then A40: rng (h + c) c= dom f1 by A36, XBOOLE_1:1;
then A41: lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = Ldiff (f1,x0) by A1, A33, A35, Th9;
A42: x0 in (dom f2) \ (f2 " {0}) by A28, A37;
rng c c= (dom f2) \ (f2 " {0})

proof

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

end;

then A43: rng c c= dom (f2 ^) by RFUNCT_1:def 2;
then A44: rng c c= (dom f1) /\ (dom (f2 ^)) by A39, XBOOLE_1:19;
A45: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A33, A35, A40, Def4;
A46: f2 /* c is non-zero by A43, RFUNCT_2:11;

A47: now

let n be Element of NAT ; :: thesis: ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) . n = ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))))) . n
thus ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) . n = ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) . n) by SEQ_1:8
.= ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) . n) - (((f1 /* c) (#) (f2 /* (h + c))) . n)) by RFUNCT_2:1
.= ((h ") . n) * ((((f1 /* (h + c)) . n) * ((f2 /* c) . n)) - (((f1 /* c) (#) (f2 /* (h + c))) . n)) by SEQ_1:8
.= ((h ") . n) * ((((((f1 /* (h + c)) . n) - ((f1 /* c) . n)) * ((f2 /* c) . n)) + (((f1 /* c) . n) * ((f2 /* c) . n))) - (((f1 /* c) . n) * ((f2 /* (h + c)) . n))) by SEQ_1:8
.= ((((h ") . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n))))
.= ((((h ") . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n)))) by RFUNCT_2:1
.= ((((h ") . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) - (f2 /* c)) . n))) by RFUNCT_2:1
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") . n) * (((f2 /* (h + c)) - (f2 /* c)) . n))) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n)) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) - (((f1 /* c) . n) * (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n)) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) - (((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) . n) by SEQ_1:8
.= ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))))) . n by RFUNCT_2:1 ; :: thesis: verum

end;

now

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

end;

then A48: (f2 /* c) + ((f2 /* (h + c)) - (f2 /* c)) = f2 /* (h + c) by FUNCT_2:63;
A49: lim h = 0 by FDIFF_1:def 1;
(dom f1) /\ ((dom f2) \ (f2 " {0})) c= (dom f2) \ (f2 " {0}) by XBOOLE_1:17;
then A50: rng (h + c) c= (dom f2) \ (f2 " {0}) by A36, XBOOLE_1:1;
then A51: rng (h + c) c= dom (f2 ^) by RFUNCT_1:def 2;
then A52: rng (h + c) c= (dom f1) /\ (dom (f2 ^)) by A40, XBOOLE_1:19;
A53: f2 /* (h + c) is non-zero by A51, RFUNCT_2:11;
then A54: (f2 /* (h + c)) (#) (f2 /* c) is non-zero by A46, SEQ_1:35;
(h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) = (h ") (#) (((f1 (#) (f2 ^)) /* (h + c)) - ((f1 / f2) /* c)) by RFUNCT_1:31
.= (h ") (#) (((f1 (#) (f2 ^)) /* (h + c)) - ((f1 (#) (f2 ^)) /* c)) by RFUNCT_1:31
.= (h ") (#) (((f1 /* (h + c)) (#) ((f2 ^) /* (h + c))) - ((f1 (#) (f2 ^)) /* c)) by A52, RFUNCT_2:8
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 (#) (f2 ^)) /* c)) by A51, RFUNCT_2:12
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) (#) ((f2 ^) /* c))) by A44, RFUNCT_2:8
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) /" (f2 /* c))) by A43, RFUNCT_2:12
.= (h ") (#) ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by A53, A46, SEQ_1:50
.= ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) /" ((f2 /* (h + c)) (#) (f2 /* c)) by SEQ_1:41 ;
then A55: (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) = ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))))) /" ((f2 /* (h + c)) (#) (f2 /* c)) by A47, FUNCT_2:63;
(dom f2) \ (f2 " {0}) c= dom f2 by XBOOLE_1:36;
then A56: rng (h + c) c= dom f2 by A50, XBOOLE_1:1;
then A57: lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = Ldiff (f2,x0) by A2, A33, A35, Th9;
Ldiff (f2,x0) = Ldiff (f2,x0) ;
then A58: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A33, A35, A56, Th9;

now

let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) . n = ((f2 /* (h + c)) - (f2 /* c)) . n
A59: h . n <> 0 by A35;
thus (h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) . n = ((h (#) (h ")) (#) ((f2 /* (h + c)) - (f2 /* c))) . n by SEQ_1:14
.= ((h (#) (h ")) . n) * (((f2 /* (h + c)) - (f2 /* c)) . n) by SEQ_1:8
.= ((h . n) * ((h ") . n)) * (((f2 /* (h + c)) - (f2 /* c)) . n) by SEQ_1:8
.= ((h . n) * ((h . n) ")) * (((f2 /* (h + c)) - (f2 /* c)) . n) by VALUED_1:10
.= 1 * (((f2 /* (h + c)) - (f2 /* c)) . n) by A59, XCMPLX_0:def 7
.= ((f2 /* (h + c)) - (f2 /* c)) . n ; :: thesis: verum

end;

then A60: h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = (f2 /* (h + c)) - (f2 /* c) by FUNCT_2:63;
A61: 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 A33, TARSKI:def 1; :: thesis: verum

end;

A62: 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 (((f1 /* c) . m) - (f1 . 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 (((f1 /* c) . m) - (f1 . x0)) < g )
assume A63: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f1 /* c) . m) - (f1 . x0)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f1 /* c) . m) - (f1 . x0)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f1 /* c) . m) - (f1 . x0)) < g )
assume n <= m ; :: thesis: abs (((f1 /* c) . m) - (f1 . x0)) < g
abs (((f1 /* c) . m) - (f1 . x0)) = abs ((f1 . (c . m)) - (f1 . x0)) by A39, FUNCT_2:108
.= abs ((f1 . x0) - (f1 . x0)) by A61
.= 0 by ABSVALUE:def 1 ;
hence abs (((f1 /* c) . m) - (f1 . x0)) < g by A63; :: thesis: verum

end;

then A64: f1 /* c is convergent by SEQ_2:def 6;
then A65: lim (f1 /* c) = f1 . x0 by A62, SEQ_2:def 7;
dom (f2 ^) = (dom f2) \ (f2 " {0}) by RFUNCT_1:def 2;
then A66: dom (f2 ^) c= dom f2 by XBOOLE_1:36;
A67: 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 (((f2 /* c) . m) - (f2 . 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 (((f2 /* c) . m) - (f2 . x0)) < g )
assume A68: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f2 /* c) . m) - (f2 . x0)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f2 /* c) . m) - (f2 . x0)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f2 /* c) . m) - (f2 . x0)) < g )
assume n <= m ; :: thesis: abs (((f2 /* c) . m) - (f2 . x0)) < g
abs (((f2 /* c) . m) - (f2 . x0)) = abs ((f2 . (c . m)) - (f2 . x0)) by A43, A66, FUNCT_2:108, XBOOLE_1:1
.= abs ((f2 . x0) - (f2 . x0)) by A61
.= 0 by ABSVALUE:def 1 ;
hence abs (((f2 /* c) . m) - (f2 . x0)) < g by A68; :: thesis: verum

end;

then A69: f2 /* c is convergent by SEQ_2:def 6;
then A70: lim (f2 /* c) = f2 . x0 by A67, SEQ_2:def 7;
A71: h is convergent by FDIFF_1:def 1;
then h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A58, SEQ_2:14;
then A72: f2 /* (h + c) is convergent by A69, A60, A48, SEQ_2:5;
then A73: (f2 /* (h + c)) (#) (f2 /* c) is convergent by A69, SEQ_2:14;
(h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A33, A35, A56, Def4;
then lim (h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) = (lim h) * (lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) by A71, SEQ_2:15
.= 0 by A49 ;
then 0 = (lim (f2 /* (h + c))) - (f2 . x0) by A69, A70, A60, A72, SEQ_2:12;
then A74: lim ((f2 /* (h + c)) (#) (f2 /* c)) = (f2 . x0) ^2 by A69, A70, A72, SEQ_2:15;
A75: lim ((f2 /* (h + c)) (#) (f2 /* c)) <> 0

proof

assume not lim ((f2 /* (h + c)) (#) (f2 /* c)) <> 0 ; :: thesis: contradiction
then f2 . x0 = 0 by A74, XCMPLX_1:6;
hence contradiction by A6, A8, A15, A12; :: thesis: verum

end;

Ldiff (f1,x0) = Ldiff (f1,x0) ;
then (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A33, A35, A40, Th9;
then A76: ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A69, SEQ_2:14;
A77: (f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A58, A64, SEQ_2:14;
then A78: (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A76, SEQ_2:11;
then lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (lim ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))))) / (lim ((f2 /* (h + c)) (#) (f2 /* c))) by A54, A73, A75, A55, SEQ_2:24
.= ((lim (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) - (lim ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))))) / (lim ((f2 /* (h + c)) (#) (f2 /* c))) by A77, A76, SEQ_2:12
.= (((lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) * (lim (f2 /* c))) - (lim ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))))) / (lim ((f2 /* (h + c)) (#) (f2 /* c))) by A45, A69, SEQ_2:15
.= (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) by A41, A58, A57, A64, A65, A70, A74, SEQ_2:15 ;
hence ( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) by A54, A73, A75, A78, A55, SEQ_2:23; :: thesis: verum

end;

[.(x0 - (min (r1,(min (r0,r2))))),x0.] c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A31, A28, XBOOLE_1:19;
then [.(x0 - (min (r1,(min (r0,r2))))),x0.] c= dom (f1 / f2) by RFUNCT_1:def 1;
hence ( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) by A17, A32, Th9; :: thesis: verum