let A be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on A & ( for x0 being Real st x0 in A holds
f . x0 <> 0 ) holds
( f ^ is_differentiable_on A & (f ^) `| A = - ((f `| A) / (f (#) f)) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on A & ( for x0 being Real st x0 in A holds
f . x0 <> 0 ) implies ( f ^ is_differentiable_on A & (f ^) `| A = - ((f `| A) / (f (#) f)) ) )
assume that
A1: f is_differentiable_on A and
A2: for x0 being Real st x0 in A holds
f . x0 <> 0 ; :: thesis: ( f ^ is_differentiable_on A & (f ^) `| A = - ((f `| A) / (f (#) f)) )

A3: now :: thesis: for x0 being Real st x0 in A holds
( f . x0 <> 0 & f is_differentiable_in x0 & f ^ is_differentiable_in x0 )

let x0 be Real; :: thesis: ( x0 in A implies ( f . x0 <> 0 & f is_differentiable_in x0 & f ^ is_differentiable_in x0 ) )
assume A4: x0 in A ; :: thesis: ( f . x0 <> 0 & f is_differentiable_in x0 & f ^ is_differentiable_in x0 )
hence A5: f . x0 <> 0 by A2; :: thesis: ( f is_differentiable_in x0 & f ^ is_differentiable_in x0 )
thus f is_differentiable_in x0 by A1, A4, FDIFF_1:9; :: thesis: f ^ is_differentiable_in x0
hence f ^ is_differentiable_in x0 by A5, Th15; :: thesis: verum

end;

then A6: for x0 being Real st x0 in A holds
f ^ is_differentiable_in x0 ;
A7: A c= dom f by A1;
A8: A c= (dom f) \ (f " {0})

proof

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

end;

then A c= dom (f ^) by RFUNCT_1:def 2;
hence A10: f ^ is_differentiable_on A by A6, FDIFF_1:9; :: thesis: (f ^) `| A = - ((f `| A) / (f (#) f))
then A11: A = dom ((f ^) `| A) by FDIFF_1:def 7;

A12: now :: thesis: for x0 being Element of REAL st x0 in dom ((f ^) `| A) holds
((f ^) `| A) . x0 = (- ((f `| A) / (f (#) f))) . x0

let x0 be Element of REAL ; :: thesis: ( x0 in dom ((f ^) `| A) implies ((f ^) `| A) . x0 = (- ((f `| A) / (f (#) f))) . x0 )
A13: dom (f `| A) = A by A1, FDIFF_1:def 7;
assume A14: x0 in dom ((f ^) `| A) ; :: thesis: ((f ^) `| A) . x0 = (- ((f `| A) / (f (#) f))) . x0
then A15: f is_differentiable_in x0 by A3, A11;
A16: f . x0 <> 0 by A3, A11, A14;
then (f . x0) * (f . x0) <> 0 ;
then (f (#) f) . x0 <> 0 by VALUED_1:5;
then not (f (#) f) . x0 in {0} by TARSKI:def 1;
then A17: not x0 in (f (#) f) " {0} by FUNCT_1:def 7;
x0 in (dom f) /\ (dom f) by A7, A11, A14;
then x0 in dom (f (#) f) by VALUED_1:def 4;
then x0 in (dom (f (#) f)) \ ((f (#) f) " {0}) by A17, XBOOLE_0:def 5;
then x0 in (dom (f `| A)) /\ ((dom (f (#) f)) \ ((f (#) f) " {0})) by A11, A14, A13, XBOOLE_0:def 4;
then A18: x0 in dom ((f `| A) / (f (#) f)) by RFUNCT_1:def 1;
thus ((f ^) `| A) . x0 = diff ((f ^),x0) by A10, A11, A14, FDIFF_1:def 7
.= - ((diff (f,x0)) / ((f . x0) ^2)) by A16, A15, Th15
.= - (((f `| A) . x0) / ((f . x0) * (f . x0))) by A1, A11, A14, FDIFF_1:def 7
.= - (((f `| A) . x0) / ((f (#) f) . x0)) by VALUED_1:5
.= - (((f `| A) . x0) * (((f (#) f) . x0) ")) by XCMPLX_0:def 9
.= - (((f `| A) / (f (#) f)) . x0) by A18, RFUNCT_1:def 1
.= (- ((f `| A) / (f (#) f))) . x0 by VALUED_1:8 ; :: thesis: verum

end;

dom (- ((f `| A) / (f (#) f))) = dom ((f `| A) / (f (#) f)) by VALUED_1:8
.= (dom (f `| A)) /\ ((dom (f (#) f)) \ ((f (#) f) " {0})) by RFUNCT_1:def 1
.= A /\ ((dom (f (#) f)) \ ((f (#) f) " {0})) by A1, FDIFF_1:def 7
.= A /\ (((dom f) /\ (dom f)) \ ((f (#) f) " {0})) by VALUED_1:def 4
.= A /\ ((dom f) \ (f " {0})) by Lm3
.= dom ((f ^) `| A) by A8, A11, XBOOLE_1:28 ;
hence (f ^) `| A = - ((f `| A) / (f (#) f)) by A12, PARTFUN1:5; :: thesis: verum