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:21
.=
(- 1) (#) ((1 (#) (((sin ^) `| Z) (#) (sin ^))) + (1 (#) (((sin ^) `| Z) (#) (sin ^))))
by RFUNCT_1:21
.=
(- 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:17
.=
((- 1) * 2) (#) (((- ((sin ^) (#) cot)) (#) (sin ^)) | Z)
by RFUNCT_1:45
.=
(((- 1) * 2) (#) ((- ((sin ^) (#) cot)) (#) (sin ^))) | Z
by RFUNCT_1:49
.=
(((- 2) (#) (- ((sin ^) (#) cot))) (#) (sin ^)) | Z
by RFUNCT_1:12
.=
((((- 2) * (- 1)) (#) ((sin ^) (#) cot)) (#) (sin ^)) | Z
by RFUNCT_1:17
.=
(2 (#) (((sin ^) (#) cot) (#) (sin ^))) | Z
by RFUNCT_1:12
.=
2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z)
by RFUNCT_1:49
;
hence
(diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z)
; verum