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

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

per cases by A26, XBOOLE_0:def 5;

suppose not x in dom f2 ; :: thesis:

hence contradiction by A13, A25; :: thesis:

end;

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

then f2 . x in {0} by FUNCT_1:def 7;
then A28: f2 . x = 0 by TARSKI:def 1;
x in dom f2 by A27, FUNCT_1:def 7;
hence contradiction by A8, A21, A25, A28; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A29: [.x0,(x0 + (min (r1,(min (r0,r2))))).] c= (dom f2) \ (f2 " {0}) by RFUNCT_1:def 2;
min (r1,(min (r0,r2))) <= r1 by XXREAL_0:17;
then A30: x0 + (min (r1,(min (r0,r2)))) <= x0 + r1 by XREAL_1:7;
then x0 <= x0 + r1 by A18, XXREAL_0:2;
then A31: x0 in [.x0,(x0 + r1).] by XXREAL_1:1;
x0 + (min (r1,(min (r0,r2)))) in { g where g is Real : ( x0 <= g & g <= x0 + r1 ) } by A18, A30;
then x0 + (min (r1,(min (r0,r2)))) in [.x0,(x0 + r1).] by RCOMP_1:def 1;
then [.x0,(x0 + (min (r1,(min (r0,r2))))).] c= [.x0,(x0 + r1).] by A31, XXREAL_2:def 12;
then A32: [.x0,(x0 + (min (r1,(min (r0,r2))))).] c= dom f1 by A6;
then [.x0,(x0 + (min (r1,(min (r0,r2))))).] c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A29, XBOOLE_1:19;
then A33: [.x0,(x0 + (min (r1,(min (r0,r2))))).] c= dom (f1 / f2) by RFUNCT_1:def 1;
A34: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 / f2) & ( for n being 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))) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis:
let c be constant Real_Sequence; :: thesis:
assume that
A35: rng c = {x0} and
A36: rng (h + c) c= dom (f1 / f2) and
A37: for n being Nat holds h . n > 0 ; :: thesis:
A38: rng (h + c) c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A36, RFUNCT_1:def 1;
( 0 <= min (r1,(min (r0,r2))) & x0 + 0 = x0 ) by A5, A17, XXREAL_0:15;
then x0 <= x0 + (min (r1,(min (r0,r2)))) by XREAL_1:7;
then A39: x0 in [.x0,(x0 + (min (r1,(min (r0,r2))))).] by XXREAL_1:1;
then A40: x0 in dom f1 by A32;
A41: rng c c= dom f1 by A35, A40, TARSKI:def 1;
(dom f1) /\ ((dom f2) \ (f2 " {0})) c= dom f1 by XBOOLE_1:17;
then A42: rng (h + c) c= dom f1 by A38;
then A43: lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = Rdiff (f1,x0) by A1, A35, A37, Th15;
A44: x0 in (dom f2) \ (f2 " {0}) by A29, A39;
rng c c= (dom f2) \ (f2 " {0}) by A35, A44, TARSKI:def 1;
then A45: rng c c= dom (f2 ^) by RFUNCT_1:def 2;
then A46: rng c c= (dom f1) /\ (dom (f2 ^)) by A41, XBOOLE_1:19;
A47: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A35, A37, A42;
A48: f2 /* c is non-zero by A45, RFUNCT_2:11;

A49: now :: thesis:

let n be Element of NAT ; :: thesis:
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:

end;

now :: thesis:

let n be Element of NAT ; :: thesis:
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:

end;

then A50: (f2 /* c) + ((f2 /* (h + c)) - (f2 /* c)) = f2 /* (h + c) by FUNCT_2:63;
(dom f1) /\ ((dom f2) \ (f2 " {0})) c= (dom f2) \ (f2 " {0}) by XBOOLE_1:17;
then A51: rng (h + c) c= (dom f2) \ (f2 " {0}) by A38;
then A52: rng (h + c) c= dom (f2 ^) by RFUNCT_1:def 2;
then A53: rng (h + c) c= (dom f1) /\ (dom (f2 ^)) by A42, XBOOLE_1:19;
A54: f2 /* (h + c) is non-zero by A52, RFUNCT_2:11;
then A55: (f2 /* (h + c)) (#) (f2 /* c) is non-zero by A48, 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 A53, RFUNCT_2:8
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 (#) (f2 ^)) /* c)) by A52, RFUNCT_2:12
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) (#) ((f2 ^) /* c))) by A46, RFUNCT_2:8
.= (h ") (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) /" (f2 /* c))) by A45, RFUNCT_2:12
.= (h ") (#) ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by A54, A48, SEQ_1:50
.= ((h ") (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) /" ((f2 /* (h + c)) (#) (f2 /* c)) by SEQ_1:41 ;
then A56: (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 A49, FUNCT_2:63;
(dom f2) \ (f2 " {0}) c= dom f2 by XBOOLE_1:36;
then A57: rng (h + c) c= dom f2 by A51;
then A58: lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = Rdiff (f2,x0) by A2, A35, A37, Th15;
A59: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A35, A37, A57;

now :: thesis:

let n be Element of NAT ; :: thesis:
A60: h . n <> 0 by A37;
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 A60, XCMPLX_0:def 7
.= ((f2 /* (h + c)) - (f2 /* c)) . n ; :: thesis:

end;

then A61: h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = (f2 /* (h + c)) - (f2 /* c) by FUNCT_2:63;
A62: for m being Element of NAT holds c . m = x0

proof

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

end;

A63: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f1 /* c) . m) - (f1 . x0)).| < g

proof

let g be Real; :: thesis:
assume A64: 0 < g ; :: thesis:
take n = 0 ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
A65: m in NAT by ORDINAL1:def 12;
|.(((f1 /* c) . m) - (f1 . x0)).| = |.((f1 . (c . m)) - (f1 . x0)).| by A41, FUNCT_2:108, A65
.= |.((f1 . x0) - (f1 . x0)).| by A62, A65
.= 0 by ABSVALUE:def 1 ;
hence |.(((f1 /* c) . m) - (f1 . x0)).| < g by A64; :: thesis:

end;

then A66: f1 /* c is convergent by SEQ_2:def 6;
then A67: lim (f1 /* c) = f1 . x0 by A63, SEQ_2:def 7;
dom (f2 ^) = (dom f2) \ (f2 " {0}) by RFUNCT_1:def 2;
then A68: dom (f2 ^) c= dom f2 by XBOOLE_1:36;
A69: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f2 /* c) . m) - (f2 . x0)).| < g

proof

let g be Real; :: thesis:
assume A70: 0 < g ; :: thesis:
take n = 0 ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
A71: m in NAT by ORDINAL1:def 12;
|.(((f2 /* c) . m) - (f2 . x0)).| = |.((f2 . (c . m)) - (f2 . x0)).| by A45, A68, FUNCT_2:108, XBOOLE_1:1, A71
.= |.((f2 . x0) - (f2 . x0)).| by A62, A71
.= 0 by ABSVALUE:def 1 ;
hence |.(((f2 /* c) . m) - (f2 . x0)).| < g by A70; :: thesis:

end;

then A72: f2 /* c is convergent by SEQ_2:def 6;
then A73: lim (f2 /* c) = f2 . x0 by A69, SEQ_2:def 7;
h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A59;
then A74: f2 /* (h + c) is convergent by A72, A61, A50;
then A75: (f2 /* (h + c)) (#) (f2 /* c) is convergent by A72;
(h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A35, A37, A57;
then lim (h (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) = (lim h) * (lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) by SEQ_2:15
.= 0 ;
then 0 = (lim (f2 /* (h + c))) - (f2 . x0) by A72, A73, A61, A74, SEQ_2:12;
then A76: lim ((f2 /* (h + c)) (#) (f2 /* c)) = (f2 . x0) ^2 by A72, A73, A74, SEQ_2:15;
A77: lim ((f2 /* (h + c)) (#) (f2 /* c)) <> 0

proof

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

end;

(h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A35, A37, A42;
then A78: ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A72;
A79: (f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A59, A66;
then A80: (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A78;
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 A55, A75, A77, A56, 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 A79, A78, 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 A47, A72, SEQ_2:15
.= (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) by A43, A59, A58, A66, A67, A73, A76, SEQ_2:15 ;
hence ( (h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)) is convergent & lim ((h ") (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) by A55, A75, A77, A80, A56, SEQ_2:23; :: thesis:

end;

0 < min (r1,(min (r0,r2))) by A5, A17, XXREAL_0:15;
hence ( f1 / f2 is_right_differentiable_in x0 & Rdiff ((f1 / f2),x0) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) by A33, A34, Th15; :: thesis: