let A be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
f2 . x0 <> 0 ) holds
( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
f2 . x0 <> 0 ) implies ( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) ) )
assume that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A and
A3: for x0 being Real st x0 in A holds
f2 . x0 <> 0 ; :: thesis: ( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )
A4: A c= dom f1 by A1;
A5: A c= dom f2 by A2;
A6: A c= (dom f2) \ (f2 " {0})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (dom f2) \ (f2 " {0}) )
assume A7: x in A ; :: thesis: x in (dom f2) \ (f2 " {0})
then reconsider x9 = x as Real ;
assume not x in (dom f2) \ (f2 " {0}) ; :: thesis: contradiction
then ( not x in dom f2 or x in f2 " {0} ) by XBOOLE_0:def 5;
then f2 . x9 in {0} by A5, A7, FUNCT_1:def 7;
then f2 . x9 = 0 by TARSKI:def 1;
hence contradiction by A3, A7; :: thesis: verum

end;

then A c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A4, XBOOLE_1:19;
then A8: A c= dom (f1 / f2) by RFUNCT_1:def 1;

A9: now :: thesis: for x0 being Real st x0 in A holds
( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )

let x0 be Real; :: thesis: ( x0 in A implies ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 ) )
assume A10: x0 in A ; :: thesis: ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
hence A11: f2 . x0 <> 0 by A3; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
thus A12: f1 is_differentiable_in x0 by A1, A10, FDIFF_1:9; :: thesis: ( f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
thus f2 is_differentiable_in x0 by A2, A10, FDIFF_1:9; :: thesis: f1 / f2 is_differentiable_in x0
hence f1 / f2 is_differentiable_in x0 by A11, A12, Th14; :: thesis: verum

end;

then for x0 being Real st x0 in A holds
f1 / f2 is_differentiable_in x0 ;
hence A13: f1 / f2 is_differentiable_on A by A8, FDIFF_1:9; :: thesis: (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)
then A14: A = dom ((f1 / f2) `| A) by FDIFF_1:def 7;

A15: now :: thesis: for x0 being Element of REAL st x0 in dom ((f1 / f2) `| A) holds
((f1 / f2) `| A) . x0 = ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in dom ((f1 / f2) `| A) implies ((f1 / f2) `| A) . x0 = ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0 )
assume A16: x0 in dom ((f1 / f2) `| A) ; :: thesis: ((f1 / f2) `| A) . x0 = ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0
then A17: f1 is_differentiable_in x0 by A9, A14;
dom (f2 `| A) = A by A2, FDIFF_1:def 7;
then x0 in (dom (f2 `| A)) /\ (dom f1) by A4, A14, A16, XBOOLE_0:def 4;
then A18: x0 in dom ((f2 `| A) (#) f1) by VALUED_1:def 4;
dom (f1 `| A) = A by A1, FDIFF_1:def 7;
then x0 in (dom (f1 `| A)) /\ (dom f2) by A5, A14, A16, XBOOLE_0:def 4;
then x0 in dom ((f1 `| A) (#) f2) by VALUED_1:def 4;
then x0 in (dom ((f1 `| A) (#) f2)) /\ (dom ((f2 `| A) (#) f1)) by A18, XBOOLE_0:def 4;
then A19: x0 in dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) by VALUED_1:12;
A20: f2 . x0 <> 0 by A9, A14, A16;
then (f2 . x0) * (f2 . x0) <> 0 ;
then (f2 (#) f2) . x0 <> 0 by VALUED_1:5;
then not (f2 (#) f2) . x0 in {0} by TARSKI:def 1;
then A21: not x0 in (f2 (#) f2) " {0} by FUNCT_1:def 7;
x0 in (dom f2) /\ (dom f2) by A5, A14, A16;
then x0 in dom (f2 (#) f2) by VALUED_1:def 4;
then x0 in (dom (f2 (#) f2)) \ ((f2 (#) f2) " {0}) by A21, XBOOLE_0:def 5;
then x0 in (dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by A19, XBOOLE_0:def 4;
then A22: x0 in dom ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) by RFUNCT_1:def 1;
A23: f2 is_differentiable_in x0 by A9, A14, A16;
thus ((f1 / f2) `| A) . x0 = diff ((f1 / f2),x0) by A13, A14, A16, FDIFF_1:def 7
.= (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) by A20, A17, A23, Th14
.= ((((f1 `| A) . x0) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) by A1, A14, A16, FDIFF_1:def 7
.= ((((f1 `| A) . x0) * (f2 . x0)) - (((f2 `| A) . x0) * (f1 . x0))) / ((f2 . x0) ^2) by A2, A14, A16, FDIFF_1:def 7
.= ((((f1 `| A) (#) f2) . x0) - (((f2 `| A) . x0) * (f1 . x0))) / ((f2 . x0) ^2) by VALUED_1:5
.= ((((f1 `| A) (#) f2) . x0) - (((f2 `| A) (#) f1) . x0)) / ((f2 . x0) ^2) by VALUED_1:5
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) . x0) / ((f2 . x0) * (f2 . x0)) by A19, VALUED_1:13
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) . x0) / ((f2 (#) f2) . x0) by VALUED_1:5
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) . x0) * (((f2 (#) f2) . x0) ") by XCMPLX_0:def 9
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0 by A22, RFUNCT_1:def 1 ; :: thesis: verum

end;

dom ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) = (dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by RFUNCT_1:def 1
.= ((dom ((f1 `| A) (#) f2)) /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by VALUED_1:12
.= (((dom (f1 `| A)) /\ (dom f2)) /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by VALUED_1:def 4
.= ((A /\ (dom f2)) /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by A1, FDIFF_1:def 7
.= (A /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by A5, XBOOLE_1:28
.= (A /\ ((dom (f2 `| A)) /\ (dom f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by VALUED_1:def 4
.= (A /\ (A /\ (dom f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by A2, FDIFF_1:def 7
.= (A /\ A) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0})) by A4, XBOOLE_1:28
.= A /\ (((dom f2) /\ (dom f2)) \ ((f2 (#) f2) " {0})) by VALUED_1:def 4
.= A /\ ((dom f2) \ (f2 " {0})) by Lm3
.= dom ((f1 / f2) `| A) by A6, A14, XBOOLE_1:28 ;
hence (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) by A15, PARTFUN1:5; :: thesis: verum