let f1, f2 be PartFunc of REAL,REAL; :: thesis:
let I be non empty Interval; :: thesis:
assume that
A1: I c= dom (f1 / f2) and
A2: f1 is_differentiable_on_interval I and
A3: f2 is_differentiable_on_interval I ; :: thesis:
reconsider J = ].(inf I),(sup I).[ as open Subset of REAL by Th2;
A4: J c= I by Th2;
A5: dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def 1;
A6: for x being set st x in I holds
f2 . x <> 0

proof

let x be set ; :: thesis:
assume x in I ; :: thesis:
then x in (dom f2) \ (f2 " {0}) by A1, A5, XBOOLE_0:def 4;
then ( x in dom f2 & not x in f2 " {0} ) by XBOOLE_0:def 5;
then not f2 . x in {0} by FUNCT_1:def 7;
hence f2 . x <> 0 by TARSKI:def 1; :: thesis:

end;

A7: now :: thesis:

assume A8: inf I in I ; :: thesis:
then inf I = lower_bound I by Lm5;
then f2 . (lower_bound I) <> 0 by A6, A8;
hence f1 / f2 is_right_differentiable_in lower_bound I by A2, A3, A8, FDIFF_3:19; :: thesis:

end;

A9: now :: thesis:

assume A10: sup I in I ; :: thesis:
then sup I = upper_bound I by Lm6;
then f2 . (upper_bound I) <> 0 by A6, A10;
hence f1 / f2 is_left_differentiable_in upper_bound I by A2, A3, A10, FDIFF_3:13; :: thesis:

end;

for x being Real st x in J holds
f2 . x <> 0 by A4, A6;
hence A11: f1 / f2 is_differentiable_on_interval I by A1, A2, A3, A7, A9, FDIFF_2:21; :: thesis:
then A12: dom ((f1 / f2) `\ I) = I by Def2;
( dom (f1 `\ I) = I & dom (f2 `\ I) = I ) by A2, A3, Def2;
then ( I = (dom (f1 `\ I)) /\ (dom f2) & I = (dom f1) /\ (dom (f2 `\ I)) ) by A2, A3, XBOOLE_1:28;
then A13: ( I = dom ((f1 `\ I) (#) f2) & I = dom (f1 (#) (f2 `\ I)) ) by VALUED_1:def 4;
A14: dom (f2 ^2) = dom (f2 (#) f2) by VALUED_1:def 8;
then A15: dom (f2 ^2) = (dom f2) /\ (dom f2) by VALUED_1:def 4;

now :: thesis:

let x be Real; :: thesis:
assume A16: x in I ; :: thesis:
(f2 ^2) . x = (f2 . x) ^2 by VALUED_1:11;
then A17: (f2 ^2) . x = (f2 . x) * (f2 . x) by SQUARE_1:def 1;
f2 . x <> 0 by A6, A16;
then (f2 ^2) . x <> 0 by A17, XCMPLX_1:6;
then not (f2 ^2) . x in {0} by TARSKI:def 1;
then not x in (f2 ^2) " {0} by FUNCT_1:def 7;
hence x in (dom (f2 ^2)) \ ((f2 ^2) " {0}) by A16, A3, A15, XBOOLE_0:def 5; :: thesis:

end;

then A18: I c= (dom (f2 ^2)) \ ((f2 ^2) " {0}) ;
A19: dom (((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) = I /\ I by A13, VALUED_1:12;
dom ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) = (dom (((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1))) /\ ((dom (f2 ^2)) \ ((f2 ^2) " {0})) by RFUNCT_1:def 1;
then A20: dom ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) = I by A18, A19, XBOOLE_1:28;
A21: for x being Element of REAL st x in dom ((f1 / f2) `\ I) holds
((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) . x

proof

let x be Element of REAL ; :: thesis:
assume A22: x in dom ((f1 / f2) `\ I) ; :: thesis:
then A23: f2 . x <> 0 by A6, A12;

per cases ;

suppose A24: x = inf I ; :: thesis:

then A25: ( ((f1 / f2) `\ I) . x = Rdiff ((f1 / f2),x) & (f1 `\ I) . x = Rdiff (f1,x) & (f2 `\ I) . x = Rdiff (f2,x) ) by A2, A3, A11, A22, A12, Def2;
( f1 is_right_differentiable_in x & f2 is_right_differentiable_in x ) by A2, A3, A22, A12, A24, Lm5;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) ^2) by A25, A23, FDIFF_3:19;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) * (f2 . x)) by SQUARE_1:def 1;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 (#) f2) . x) by A22, A12, A3, A15, A14, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 (#) f2) . x) by A22, A12, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 ^2) . x) by VALUED_1:def 8;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) . x) - (((f2 `\ I) (#) f1) . x)) * (((f2 ^2) . x) ") by A22, A12, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) . x) * (((f2 ^2) . x) ") by A22, A12, A19, VALUED_1:13;
hence ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) . x by A22, A12, A20, RFUNCT_1:def 1; :: thesis:

end;

suppose A26: x = sup I ; :: thesis:

then A27: ( ((f1 / f2) `\ I) . x = Ldiff ((f1 / f2),x) & (f1 `\ I) . x = Ldiff (f1,x) & (f2 `\ I) . x = Ldiff (f2,x) ) by A2, A3, A11, A22, A12, Def2;
( f1 is_left_differentiable_in x & f2 is_left_differentiable_in x ) by A2, A3, A22, A12, A26, Lm6;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) ^2) by A27, A23, FDIFF_3:13;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) * (f2 . x)) by SQUARE_1:def 1;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 (#) f2) . x) by A22, A12, A3, A15, A14, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 (#) f2) . x) by A22, A12, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 ^2) . x) by VALUED_1:def 8;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) . x) - (((f2 `\ I) (#) f1) . x)) * (((f2 ^2) . x) ") by A22, A12, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) . x) * (((f2 ^2) . x) ") by A22, A12, A19, VALUED_1:13;
hence ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) . x by A22, A12, A20, RFUNCT_1:def 1; :: thesis:

end;

suppose A28: ( x <> inf I & x <> sup I ) ; :: thesis:

then x in J by A22, A12, Th3;
then A29: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, A3, FDIFF_1:9;
( (f1 `\ I) . x = diff (f1,x) & (f2 `\ I) . x = diff (f2,x) & ((f1 / f2) `\ I) . x = diff ((f1 / f2),x) ) by A2, A3, A11, A22, A12, A28, Def2;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) ^2) by A29, A23, FDIFF_2:14;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) * (f2 . x)) by SQUARE_1:def 1;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 (#) f2) . x) by A22, A12, A3, A15, A14, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 (#) f2) . x) by A22, A12, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 ^2) . x) by VALUED_1:def 8;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) . x) - (((f2 `\ I) (#) f1) . x)) * (((f2 ^2) . x) ") by A22, A12, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) . x) * (((f2 ^2) . x) ") by A22, A12, A19, VALUED_1:13;
hence ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) . x by A22, A12, A20, RFUNCT_1:def 1; :: thesis:

end;

hence (f1 / f2) `\ I = (((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2) by A12, A20, PARTFUN1:5; :: thesis:

hereby :: thesis:

let x be Real; :: thesis:
assume A30: x in I ; :: thesis:
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2)) . x by A12, A21;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) . x) * (((f2 ^2) . x) ") by A30, A20, RFUNCT_1:def 1;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) (#) f2) . x) - (((f2 `\ I) (#) f1) . x)) * (((f2 ^2) . x) ") by A30, A19, VALUED_1:13;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) * (((f2 ^2) . x) ") by A30, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) (#) f1) . x)) / ((f2 (#) f2) . x) by VALUED_1:def 8;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 (#) f2) . x) by A30, A13, VALUED_1:def 4;
then ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) * (f2 . x)) by A30, A3, A15, A14, VALUED_1:def 4;
hence ((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) ^2) by SQUARE_1:def 1; :: thesis:

end;