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 )) ) )
assume A1: ( f . x0 <> 0 & f is_differentiable_in x0 ) ; :: thesis: ( 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;
A2: dom f1 = dom f by FUNCOP_1:19;
consider N being Neighbourhood of x0 such that
A3: N c= dom f by A1, Th11;
A4: 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 )
assume x in {1} ; :: thesis: x in rng f1
then A5: x = 1 by TARSKI:def 1;
A6: x0 in N by RCOMP_1:37;
then f1 . x0 = x by A3, A5, FUNCOP_1:13;
hence x in rng f1 by A2, A3, A6, FUNCT_1:def 5; :: thesis: verum

end;

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

now

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

end;

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