let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds
f . x0 <> 0 ) holds
(diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds
f . x0 <> 0 ) implies (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) )
assume that
A1: f is_differentiable_on 2,Z and
A2: for x0 being Real st x0 in Z holds
f . x0 <> 0 ; :: thesis: (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))
A3: f is_differentiable_on Z by A1, Th7;
then A4: f ^ is_differentiable_on Z by A2, FDIFF_2:22;
A5: Z c= dom f by A3, FDIFF_1:def 6;
A6: for x0 being Real st x0 in Z holds
(f (#) f) . x0 <> 0

proof

let x0 be Real; :: thesis: ( x0 in Z implies (f (#) f) . x0 <> 0 )
assume A7: x0 in Z ; :: thesis: (f (#) f) . x0 <> 0
then A8: f . x0 <> 0 by A2;
dom (f (#) f) = (dom f) /\ (dom f) by VALUED_1:def 4
.= dom f ;
then (f (#) f) . x0 = (f . x0) * (f . x0) by A5, A7, VALUED_1:def 4;
hence (f (#) f) . x0 <> 0 by A8, XCMPLX_1:6; :: thesis: verum

end;

(diff (f,Z)) . 1 = (diff (f,Z)) . (1 + 0)
.= ((diff (f,Z)) . 0) `| Z by TAYLOR_1:def 5
.= (f | Z) `| Z by TAYLOR_1:def 5
.= f `| Z by A3, FDIFF_2:16 ;
then A9: f `| Z is_differentiable_on Z by A1;
then (f | Z) `| Z is_differentiable_on Z by A3, FDIFF_2:16;
then A10: ((diff (f,Z)) . 0) `| Z is_differentiable_on Z by TAYLOR_1:def 5;
A11: f (#) f is_differentiable_on Z by A3, FDIFF_2:20;
then A12: (f `| Z) / (f (#) f) is_differentiable_on Z by A9, A6, FDIFF_2:21;
(diff ((f ^),Z)) . 2 = (diff ((f ^),Z)) . (1 + 1)
.= ((diff ((f ^),Z)) . (1 + 0)) `| Z by TAYLOR_1:def 5
.= (((diff ((f ^),Z)) . 0) `| Z) `| Z by TAYLOR_1:def 5
.= (((f ^) | Z) `| Z) `| Z by TAYLOR_1:def 5
.= ((f ^) `| Z) `| Z by A4, FDIFF_2:16
.= (- ((f `| Z) / (f (#) f))) `| Z by A2, A3, FDIFF_2:22
.= (- 1) (#) (((f `| Z) / (f (#) f)) `| Z) by A12, FDIFF_2:19
.= (- 1) (#) (((((f `| Z) `| Z) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by A9, A11, A6, FDIFF_2:21
.= (- 1) (#) (((((diff (f,Z)) . 2) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by A1, Lm3, Th7
.= (- 1) (#) (((((diff (f,Z)) . 2) (#) (f (#) f)) - ((((f `| Z) (#) f) + (f (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by A3, FDIFF_2:20
.= (- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((f `| Z) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:11
.= (- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((1 (#) (f `| Z)) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:21
.= (- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((1 (#) (f `| Z)) + (1 (#) (f `| Z)))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:21
.= (- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((1 + 1) (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by Th5
.= (- 1) (#) (((f (#) (((diff (f,Z)) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:9
.= ((- 1) (#) ((f (#) (((diff (f,Z)) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z)))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:32
.= (((f (#) (2 (#) (f `| Z))) (#) (f `| Z)) - (f (#) (((diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:19
.= ((f (#) ((2 (#) (f `| Z)) (#) (f `| Z))) - (f (#) (((diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:9
.= (f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:15
.= (f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f))) / (f (#) (f (#) (f (#) f))) by RFUNCT_1:9
.= (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) by RFUNCT_1:34 ;
then A13: (diff ((f ^),Z)) . 2 = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))
.= (((dom f) \ (f " {0})) --> 1) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) by Lm4 ;
A14: dom ((diff (f,Z)) . (1 + 1)) = dom (((diff (f,Z)) . (0 + 1)) `| Z) by TAYLOR_1:def 5
.= dom ((((diff (f,Z)) . 0) `| Z) `| Z) by TAYLOR_1:def 5
.= Z by A10, FDIFF_1:def 7 ;
A15: dom (((diff (f,Z)) . 2) (#) f) = (dom ((diff (f,Z)) . 2)) /\ (dom f) by VALUED_1:def 4
.= Z /\ (dom f) by A14 ;
A16: dom ((2 (#) (f `| Z)) (#) (f `| Z)) = dom (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:13
.= dom ((f `| Z) (#) (f `| Z)) by VALUED_1:def 5
.= (dom (f `| Z)) /\ (dom (f `| Z)) by VALUED_1:def 4
.= dom (f `| Z)
.= Z by A3, FDIFF_1:def 7 ;
set g1 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f));
set g2 = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)));
A17: dom (f (#) (f (#) f)) = (dom f) /\ (dom (f (#) f)) by VALUED_1:def 4
.= (dom f) /\ ((dom f) /\ (dom f)) by VALUED_1:def 4
.= (dom f) /\ (dom f)
.= dom f ;
A18: f / f = ((dom f) \ (f " {0})) --> 1 by Lm4;
then A19: dom (f / f) = (dom f) \ (f " {0}) by FUNCOP_1:13;
A20: dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = (dom (f / f)) /\ (dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) by VALUED_1:def 4;
then A21: dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) c= dom (f / f) by XBOOLE_1:17;
A22: for x being Element of REAL st x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) holds
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) implies ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x )
assume A23: x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) ; :: thesis: ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x
.= ((f / f) . x) * (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x) by A23, VALUED_1:def 4
.= 1 * (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x) by A18, A19, A21, A23, FUNCOP_1:7
.= ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x ;
hence ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x ; :: thesis: verum

end;

dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) = (dom (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0})) by RFUNCT_1:def 1
.= ((dom ((2 (#) (f `| Z)) (#) (f `| Z))) /\ (dom (((diff (f,Z)) . 2) (#) f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0})) by VALUED_1:12
.= (Z /\ (dom (((diff (f,Z)) . 2) (#) f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0})) by A16
.= (Z /\ (Z /\ (dom f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0})) by A15
.= ((Z /\ Z) /\ (dom f)) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0})) by XBOOLE_1:16
.= (Z /\ (dom f)) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
.= (Z /\ (dom f)) /\ ((dom f) \ ((f (#) (f (#) f)) " {0})) by A17
.= ((Z /\ (dom f)) /\ (dom f)) \ ((f (#) (f (#) f)) " {0}) by XBOOLE_1:49
.= (Z /\ ((dom f) /\ (dom f))) \ ((f (#) (f (#) f)) " {0}) by XBOOLE_1:16
.= (Z /\ (dom f)) \ ((f (#) (f (#) f)) " {0})
.= Z \ ((f (#) (f (#) f)) " {0}) by A5, XBOOLE_1:28
.= Z \ (f " {0}) by Lm5 ;
then dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) by A5, A19, A20, XBOOLE_1:28, XBOOLE_1:33;
hence (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) by A18, A13, A22, PARTFUN1:5; :: thesis: verum