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 A1: ( f1 is_left_differentiable_in x0 & 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 ) ) )
given r0 being Real such that A2: ( r0 > 0 & ( 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 r1 being Real such that
A3: ( 0 < r1 & [.(x0 - r1),x0.] c= dom f1 ) by A1, Def4;
consider r2 being Real such that
A4: ( 0 < r2 & [.(x0 - r2),x0.] c= dom f2 ) by A1, Def4;
set r3 = min r0,r2;
A5: 0 < min r0,r2 by A2, A4, XXREAL_0:15;
then A6: x0 - (min r0,r2) <= x0 by XREAL_1:45;
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 A6;
then A8: x0 - (min r0,r2) in [.(x0 - r0),x0.] by RCOMP_1:def 1;
x0 - r0 <= x0 by A6, 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 A6;
then A12: x0 - (min r0,r2) in [.(x0 - r2),x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A6, 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 f2 by A4, XBOOLE_1:1;
set r = min r1,(min r0,r2);
A15: 0 < min r1,(min r0,r2) by A3, A5, XXREAL_0:15;
then A16: x0 - (min r1,(min r0,r2)) <= x0 by XREAL_1:45;
min r1,(min r0,r2) <= r1 by XXREAL_0:17;
then A17: x0 - r1 <= x0 - (min r1,(min r0,r2)) by XREAL_1:15;
then x0 - (min r1,(min r0,r2)) in { g where g is Real : ( x0 - r1 <= g & g <= x0 ) } by A16;
then A18: x0 - (min r1,(min r0,r2)) in [.(x0 - r1),x0.] by RCOMP_1:def 1;
x0 - r1 <= x0 by A16, A17, XXREAL_0:2;
then x0 in [.(x0 - r1),x0.] by XXREAL_1:1;
then A19: [.(x0 - (min r1,(min r0,r2))),x0.] c= [.(x0 - r1),x0.] by A18, XXREAL_2:def 12;
min r1,(min r0,r2) <= min r0,r2 by XXREAL_0:17;
then A20: x0 - (min r0,r2) <= x0 - (min r1,(min r0,r2)) by XREAL_1:15;
then x0 - (min r1,(min r0,r2)) in { g where g is Real : ( x0 - (min r0,r2) <= g & g <= x0 ) } by A16;
then A21: x0 - (min r1,(min r0,r2)) in [.(x0 - (min r0,r2)),x0.] by RCOMP_1:def 1;
x0 - (min r0,r2) <= x0 by A16, A20, XXREAL_0:2;
then x0 in [.(x0 - (min r0,r2)),x0.] by XXREAL_1:1;
then A22: [.(x0 - (min r1,(min r0,r2))),x0.] c= [.(x0 - (min r0,r2)),x0.] by A21, XXREAL_2:def 12;
A23: [.(x0 - (min r1,(min r0,r2))),x0.] c= dom f1 by A3, A19, XBOOLE_1:1;
[.(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
A24: ( x in [.(x0 - (min r1,(min r0,r2))),x0.] & not x in dom (f2 ^ ) ) by TARSKI:def 3;
reconsider x = x as Real by A24;
A25: not x in (dom f2) \ (f2 " {0 }) by A24, RFUNCT_1:def 8;
A26: x in [.(x0 - (min r0,r2)),x0.] by A22, A24;

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

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then A27: [.(x0 - (min r1,(min r0,r2))),x0.] c= (dom f2) \ (f2 " {0 }) by RFUNCT_1:def 8;
then [.(x0 - (min r1,(min r0,r2))),x0.] c= (dom f1) /\ ((dom f2) \ (f2 " {0 })) by A23, XBOOLE_1:19;
then A28: [.(x0 - (min r1,(min r0,r2))),x0.] c= dom (f1 / f2) by RFUNCT_1:def 4;
for h being convergent_to_0 Real_Sequence
for c being V6 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 V6 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 V6 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
A29: rng c = {x0} and
A30: rng (h + c) c= dom (f1 / f2) and
A31: 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 ) )
A32: rng (h + c) c= (dom f1) /\ ((dom f2) \ (f2 " {0 })) by A30, RFUNCT_1:def 4;
( (dom f1) /\ ((dom f2) \ (f2 " {0 })) c= dom f1 & (dom f1) /\ ((dom f2) \ (f2 " {0 })) c= (dom f2) \ (f2 " {0 }) ) by XBOOLE_1:17;
then A33: ( rng (h + c) c= dom f1 & rng (h + c) c= (dom f2) \ (f2 " {0 }) ) by A32, XBOOLE_1:1;
(dom f2) \ (f2 " {0 }) c= dom f2 by XBOOLE_1:36;
then A34: rng (h + c) c= dom f2 by A33, XBOOLE_1:1;
Ldiff f1,x0 = Ldiff f1,x0 ;
then A35: ( (h " ) (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent & lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) = Ldiff f1,x0 ) by A1, A29, A31, A33, Th9;
Ldiff f2,x0 = Ldiff f2,x0 ;
then A36: ( (h " ) (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent & lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) = Ldiff f2,x0 ) by A1, A29, A31, A34, Th9;
A37: rng (h + c) c= dom (f2 ^ ) by A33, RFUNCT_1:def 8;
then A38: rng (h + c) c= (dom f1) /\ (dom (f2 ^ )) by A33, XBOOLE_1:19;
A39: f2 /* (h + c) is non-zero by A37, RFUNCT_2:26;
A40: 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 A29, TARSKI:def 1; :: thesis: verum

end;

0 <= min r1,(min r0,r2) by A3, A5, XXREAL_0:15;
then x0 - (min r1,(min r0,r2)) <= x0 by XREAL_1:45;
then A41: x0 in [.(x0 - (min r1,(min r0,r2))),x0.] by XXREAL_1:1;
then A42: x0 in dom f1 by A23;
A43: 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 A29, A42, TARSKI:def 1; :: thesis: verum

end;

A44: 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 A45: 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 A43, FUNCT_2:185
.= abs ((f1 . x0) - (f1 . x0)) by A40
.= 0 by ABSVALUE:def 1 ;
hence abs (((f1 /* c) . m) - (f1 . x0)) < g by A45; :: thesis: verum

end;

A46: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A47: f1 /* c is convergent by A44, SEQ_2:def 6;
then A48: lim (f1 /* c) = f1 . x0 by A44, SEQ_2:def 7;
A49: ( (h " ) (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent & (h " ) (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent ) by A1, A29, A31, A33, A34, Def4;
A50: x0 in (dom f2) \ (f2 " {0 }) by A27, A41;
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 A29, A50, TARSKI:def 1; :: thesis: verum

end;

then A51: rng c c= dom (f2 ^ ) by RFUNCT_1:def 8;
then A52: rng c c= (dom f1) /\ (dom (f2 ^ )) by A43, XBOOLE_1:19;
A53: f2 /* c is non-zero by A51, RFUNCT_2:26;
then A54: (f2 /* (h + c)) (#) (f2 /* c) is non-zero by A39, SEQ_1:43;
dom (f2 ^ ) = (dom f2) \ (f2 " {0 }) by RFUNCT_1:def 8;
then A55: dom (f2 ^ ) c= dom f2 by XBOOLE_1:36;
A56: 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 A57: 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 A51, A55, FUNCT_2:185, XBOOLE_1:1
.= abs ((f2 . x0) - (f2 . x0)) by A40
.= 0 by ABSVALUE:def 1 ;
hence abs (((f2 /* c) . m) - (f2 . x0)) < g by A57; :: thesis: verum

end;

then A58: f2 /* c is convergent by SEQ_2:def 6;
then A59: lim (f2 /* c) = f2 . x0 by A56, SEQ_2:def 7;
A60: h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A36, A46, SEQ_2:28;
A61: h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) = (f2 /* (h + c)) - (f2 /* c)

proof

now

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

end;

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

end;

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

proof

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

end;

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

end;

then A63: f2 /* (h + c) is convergent by A58, A60, A61, SEQ_2:19;
lim (h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = (lim h) * (lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) by A46, A49, SEQ_2:29
.= 0 by A46 ;
then A64: 0 = (lim (f2 /* (h + c))) - (f2 . x0) by A58, A59, A61, A63, SEQ_2:26;
A65: (f2 /* (h + c)) (#) (f2 /* c) is convergent by A58, A63, SEQ_2:28;
A66: lim ((f2 /* (h + c)) (#) (f2 /* c)) = (f2 . x0) ^2 by A58, A59, A63, A64, SEQ_2:29;
A67: lim ((f2 /* (h + c)) (#) (f2 /* c)) <> 0

proof

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

end;

A68: (f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A36, A47, SEQ_2:28;
A69: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A35, A58, SEQ_2:28;
A70: (h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) = (h " ) (#) (((f1 (#) (f2 ^ )) /* (h + c)) - ((f1 / f2) /* c)) by RFUNCT_1:47
.= (h " ) (#) (((f1 (#) (f2 ^ )) /* (h + c)) - ((f1 (#) (f2 ^ )) /* c)) by RFUNCT_1:47
.= (h " ) (#) (((f1 /* (h + c)) (#) ((f2 ^ ) /* (h + c))) - ((f1 (#) (f2 ^ )) /* c)) by A38, RFUNCT_2:23
.= (h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 (#) (f2 ^ )) /* c)) by A37, RFUNCT_2:27
.= (h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) (#) ((f2 ^ ) /* c))) by A52, RFUNCT_2:23
.= (h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) /" (f2 /* c))) by A51, RFUNCT_2:27
.= (h " ) (#) ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by A39, A53, SEQ_1:58
.= ((h " ) (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) /" ((f2 /* (h + c)) (#) (f2 /* c)) by SEQ_1:49 ;
A71: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A68, A69, SEQ_2:25;

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:12
.= ((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) . n) - (((f1 /* c) (#) (f2 /* (h + c))) . n)) by RFUNCT_2:6
.= ((h " ) . n) * ((((f1 /* (h + c)) . n) * ((f2 /* c) . n)) - (((f1 /* c) (#) (f2 /* (h + c))) . n)) by SEQ_1:12
.= ((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:12
.= ((((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:6
.= ((((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:6
.= ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h " ) . n) * (((f2 /* (h + c)) - (f2 /* c)) . n))) by SEQ_1:12
.= ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) . n)) by SEQ_1:12
.= ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) - (((f1 /* c) . n) * (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) . n)) by SEQ_1:12
.= ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) - (((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) . n) by SEQ_1:12
.= ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) . n by RFUNCT_2:6 ; :: thesis: verum

end;

then A72: (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 A70, FUNCT_2:113;
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, A65, A67, A71, SEQ_2:38
.= ((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 A68, A69, SEQ_2:26
.= (((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 A49, A58, SEQ_2:29
.= (((Ldiff f1,x0) * (f2 . x0)) - ((Ldiff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A35, A36, A47, A48, A59, A66, SEQ_2:29 ;
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, A65, A67, A71, A72, SEQ_2:37; :: thesis: verum

end;

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 A15, A28, Th9; :: thesis: verum