let Z be open Subset of REAL ; ( Z c= dom cot implies (diff cot ,Z) . 2 = 2 (#) (((cot (#) (sin ^ )) (#) (sin ^ )) | Z) )
assume A1:
Z c= dom cot
; (diff cot ,Z) . 2 = 2 (#) (((cot (#) (sin ^ )) (#) (sin ^ )) | Z)
then A2:
cot is_differentiable_on Z
by Th59;
A3:
sin ^ is_differentiable_on Z
by A1, Th60;
then A4:
(sin ^ ) (#) (sin ^ ) is_differentiable_on Z
by FDIFF_2:20;
then A5:
(- 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 A1, Th59
.=
((- 1) (#) ((sin ^ ) (#) (sin ^ ))) `| Z
by A5, FDIFF_2:16
.=
(- 1) (#) (((sin ^ ) (#) (sin ^ )) `| Z)
by A4, 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 Th5
.=
(- 1) (#) (2 (#) (((- ((sin ^ ) (#) cot )) | Z) (#) (sin ^ )))
by A1, Th60
.=
((- 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)
; verum