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 ThB19, A1;
then A4: f ^ is_differentiable_on Z by A2, FDIFF_2:22;
A: 1 <= 2 - 1 ;
A5: (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 ;
A6: f `| Z is_differentiable_on Z by A5, A1, A, TAYLOR_1:def 6;
A7: f (#) f is_differentiable_on Z by A3, FDIFF_2:20;
A10: Z c= dom f by A3, FDIFF_1:def 7;
A8: 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 A9: x0 in Z ; :: thesis: (f (#) f) . x0 <> 0
dom (f (#) f) = (dom f) /\ (dom f) by VALUED_1:def 4
.= dom f ;
then A12: (f (#) f) . x0 = (f . x0) * (f . x0) by A9, A10, VALUED_1:def 4;
f . x0 <> 0 by A9, A2;
hence (f (#) f) . x0 <> 0 by A12, XCMPLX_1:6; :: thesis: verum

end;

A13: (f `| Z) / (f (#) f) is_differentiable_on Z by A8, A7, A6, FDIFF_2:21;
set f1 = f `| Z;
set f2 = f (#) f;
X4: (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 A3, A2, FDIFF_2:22
.= (- 1) (#) (((f `| Z) / (f (#) f)) `| Z) by A13, FDIFF_2:19
.= (- 1) (#) (((((f `| Z) `| Z) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by A8, A7, A6, FDIFF_2:21
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by Lm1, ThB19, A1
.= (- 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:23
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f ^2 )) - ((f (#) ((1 (#) (f `| Z)) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:33
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f ^2 )) - ((f (#) ((1 (#) (f `| Z)) + (1 (#) (f `| Z)))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:33
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f ^2 )) - ((f (#) ((1 + 1) (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by ThB2
.= (- 1) (#) (((f (#) (((diff f,Z) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:21
.= ((- 1) (#) ((f (#) (((diff f,Z) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z)))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:48
.= (((f (#) (2 (#) (f `| Z))) (#) (f `| Z)) - (f (#) (((diff f,Z) . 2) (#) f))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:31
.= ((f (#) ((2 (#) (f `| Z)) (#) (f `| Z))) - (f (#) (((diff f,Z) . 2) (#) f))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:21
.= (f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f))) / ((f (#) f) (#) (f (#) f)) by RFUNCT_1:27
.= (f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f))) / (f (#) (f (#) (f (#) f))) by RFUNCT_1:21
.= (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) by RFUNCT_1:50 ;
X1: f / f = ((dom f) \ (f " {0 })) --> 1 by Lem1;
then x1: dom (f / f) = (dom f) \ (f " {0 }) by FUNCOP_1:19;
K1: Z c= dom f by A10;
H4: dom ((2 (#) (f `| Z)) (#) (f `| Z)) = dom (2 (#) ((f `| Z) (#) (f `| Z))) by RFUNCT_1:25
.= 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 8 ;
f `| Z = (f | Z) `| Z by A3, FDIFF_2:16;
then (f | Z) `| Z is_differentiable_on Z by A6;
then H1: ((diff f,Z) . 0 ) `| Z is_differentiable_on Z by TAYLOR_1:def 5;
H2: 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 H1, FDIFF_1:def 8 ;
H3: dom (((diff f,Z) . 2) (#) f) = (dom ((diff f,Z) . 2)) /\ (dom f) by VALUED_1:def 4
.= Z /\ (dom f) by H2 ;
H5: 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 ;
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 4
.= ((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 H4
.= (Z /\ (Z /\ (dom f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0 })) by H3
.= ((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 H5
.= ((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 K1, XBOOLE_1:28
.= Z \ (f " {0 }) by Lem4 ;
then dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) c= (dom f) \ (f " {0 }) by A10, XBOOLE_1:33;
then ZX: dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) c= dom (f / f) by x1;
XX: (diff (f ^ ),Z) . 2 = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) by X4
.= (((dom f) \ (f " {0 })) --> 1) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) by Lem1 ;
set g2 = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f)));
set g1 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f));
H3: 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 H1: dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f)))) c= dom (f / f) by XBOOLE_1:17;
dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) c= dom (f / f) by ZX;
then B1: 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 H3, XBOOLE_1:28;
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 C1: 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
then x in dom (f / f) by H1;
then C2: x in (dom f) \ (f " {0 }) by x1;
((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 C1, VALUED_1:def 4
.= 1 * (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) . x) by X1, C2, FUNCOP_1:13
.= ((((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;

then (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f)) = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) by B1, PARTFUN1:34;
hence (diff (f ^ ),Z) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f)) by XX, X1; :: thesis: verum