let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f . x0 <> 0 & f is_differentiable_in x0 holds
( f ^ is_differentiable_in x0 & diff (f ^ ),x0 = - ((diff f,x0) / ((f . x0) ^2 )) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f . x0 <> 0 & f is_differentiable_in x0 implies ( f ^ is_differentiable_in x0 & diff (f ^ ),x0 = - ((diff f,x0) / ((f . x0) ^2 )) ) )
reconsider f1 = (dom f) --> 1 as PartFunc of (dom f),REAL by FUNCOP_1:57;
dom f1 c= REAL by RELAT_1:def 18;
then reconsider f1 = f1 as PartFunc of REAL ,REAL by RELSET_1:13;
assume that
A1: f . x0 <> 0 and
A2: f is_differentiable_in x0 ; :: thesis: ( f ^ is_differentiable_in x0 & diff (f ^ ),x0 = - ((diff f,x0) / ((f . x0) ^2 )) )
consider N being Neighbourhood of x0 such that
A3: N c= dom f by A2, Th11;
A4: x0 in N by RCOMP_1:37;
A5: dom f1 = dom f by FUNCOP_1:19;
A6: rng f1 = {1}

proof

thus rng f1 c= {1} by FUNCOP_1:19; :: according to XBOOLE_0:def 10 :: thesis: {1} c= rng f1
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in rng f1 )
A7: x0 in N by RCOMP_1:37;
assume x in {1} ; :: thesis: x in rng f1
then x = 1 by TARSKI:def 1;
then f1 . x0 = x by A3, A7, FUNCOP_1:13;
hence x in rng f1 by A5, A3, A7, FUNCT_1:def 5; :: thesis: verum

end;

then A8: f1 is_differentiable_on N by A5, A3, FDIFF_1:19;
then A9: f1 is_differentiable_in x0 by A4, FDIFF_1:16;
0 = (f1 `| N) . x0 by A5, A3, A6, FDIFF_1:19, RCOMP_1:37
.= diff f1,x0 by A8, A4, FDIFF_1:def 8 ;
then diff (f1 / f),x0 = ((0 * (f . x0)) - ((diff f,x0) * (f1 . x0))) / ((f . x0) ^2 ) by A1, A2, A9, Th14;
then A10: diff (f1 / f),x0 = (- ((diff f,x0) * (f1 . x0))) / ((f . x0) ^2 )
.= (- ((diff f,x0) * 1)) / ((f . x0) ^2 ) by A3, A4, FUNCOP_1:13
.= - ((diff f,x0) / ((f . x0) ^2 )) by XCMPLX_1:188 ;
A11: dom (f1 / f) = (dom f1) /\ ((dom f) \ (f " {0 })) by RFUNCT_1:def 4
.= (dom f) \ (f " {0 }) by A5, XBOOLE_1:28, XBOOLE_1:36
.= dom (f ^ ) by RFUNCT_1:def 8 ;
A12: (dom f) \ (f " {0 }) c= dom f1 by A5, XBOOLE_1:36;

A13: now

A14: (dom f) \ (f " {0 }) = dom (f ^ ) by RFUNCT_1:def 8;
let r be Real; :: thesis: ( r in dom (f1 / f) implies (f1 / f) . r = (f ^ ) . r )
assume A15: r in dom (f1 / f) ; :: thesis: (f1 / f) . r = (f ^ ) . r
thus (f1 / f) . r = (f1 . r) * ((f . r) " ) by A15, RFUNCT_1:def 4
.= 1 * ((f . r) " ) by A5, A12, A11, A15, A14, FUNCOP_1:13
.= (f ^ ) . r by A11, A15, RFUNCT_1:def 8 ; :: thesis: verum

end;

f1 / f is_differentiable_in x0 by A1, A2, A9, Th14;
hence ( f ^ is_differentiable_in x0 & diff (f ^ ),x0 = - ((diff f,x0) / ((f . x0) ^2 )) ) by A10, A11, A13, PARTFUN1:34; :: thesis: verum