let Z be open Subset of REAL ; :: thesis: ( Z c= dom cot implies (diff cot ,Z) . 2 = 2 (#) (((cot (#) (sin ^ )) (#) (sin ^ )) | Z) )
assume A1: Z c= dom cot ; :: thesis: (diff cot ,Z) . 2 = 2 (#) (((cot (#) (sin ^ )) (#) (sin ^ )) | Z)
A2: cot is_differentiable_on Z by A1, ThB14;
A3: sin ^ is_differentiable_on Z by ThB15, A1;
then A: (sin ^ ) (#) (sin ^ ) is_differentiable_on Z by FDIFF_2:20;
then A4: (- 1) (#) ((sin ^ ) (#) (sin ^ )) is_differentiable_on Z by FDIFF_2:19;
(diff cot ,Z) . 2 = (diff cot ,Z) . (1 + 1)
.= ((diff cot ,Z) . (1 + 0 )) `| Z by TAYLOR_1:def 5
.= (((diff cot ,Z) . 0 ) `| Z) `| Z by TAYLOR_1:def 5
.= ((cot | Z) `| Z) `| Z by TAYLOR_1:def 5
.= (cot `| Z) `| Z by A2, FDIFF_2:16
.= (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) `| Z by ThB14, A1
.= ((- 1) (#) ((sin ^ ) (#) (sin ^ ))) `| Z by A4, FDIFF_2:16
.= (- 1) (#) (((sin ^ ) (#) (sin ^ )) `| Z) by A, FDIFF_2:19
.= (- 1) (#) ((((sin ^ ) `| Z) (#) (sin ^ )) + (((sin ^ ) `| Z) (#) (sin ^ ))) by A3, FDIFF_2:20
.= (- 1) (#) ((1 (#) (((sin ^ ) `| Z) (#) (sin ^ ))) + (((sin ^ ) `| Z) (#) (sin ^ ))) by RFUNCT_1:33
.= (- 1) (#) ((1 (#) (((sin ^ ) `| Z) (#) (sin ^ ))) + (1 (#) (((sin ^ ) `| Z) (#) (sin ^ )))) by RFUNCT_1:33
.= (- 1) (#) ((1 + 1) (#) (((sin ^ ) `| Z) (#) (sin ^ ))) by ThB2
.= (- 1) (#) (2 (#) (((- ((sin ^ ) (#) cot )) | Z) (#) (sin ^ ))) by ThB15, A1
.= ((- 1) * 2) (#) (((- ((sin ^ ) (#) cot )) | Z) (#) (sin ^ )) by RFUNCT_1:29
.= ((- 1) * 2) (#) (((- ((sin ^ ) (#) cot )) (#) (sin ^ )) | Z) by RFUNCT_1:61
.= (((- 1) * 2) (#) ((- ((sin ^ ) (#) cot )) (#) (sin ^ ))) | Z by RFUNCT_1:65
.= (((- 2) (#) (- ((sin ^ ) (#) cot ))) (#) (sin ^ )) | Z by RFUNCT_1:24
.= ((((- 2) * (- 1)) (#) ((sin ^ ) (#) cot )) (#) (sin ^ )) | Z by RFUNCT_1:29
.= (2 (#) (((sin ^ ) (#) cot ) (#) (sin ^ ))) | Z by RFUNCT_1:24
.= 2 (#) (((cot (#) (sin ^ )) (#) (sin ^ )) | Z) by RFUNCT_1:65 ;
hence (diff cot ,Z) . 2 = 2 (#) (((cot (#) (sin ^ )) (#) (sin ^ )) | Z) ; :: thesis: verum