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 = (f / f) (#) ((((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 = (f / f) (#) ((((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 = (f / f) (#) ((((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;
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
A10: Z c= dom f by A3, FDIFF_1:def 7;
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;
(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 (#) f)) - ((f (#) ((f `| Z) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:23
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f (#) f)) - ((f (#) ((1 (#) (f `| Z)) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:33
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f (#) f)) - ((f (#) ((1 (#) (f `| Z)) + (1 (#) (f `| Z)))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f))) by RFUNCT_1:33
.= (- 1) (#) (((((diff f,Z) . 2) (#) (f (#) f)) - ((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 ;
hence (diff (f ^ ),Z) . 2 = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff f,Z) . 2) (#) f)) / (f (#) (f (#) f))) ; :: thesis: verum