let Z be open Subset of REAL ; :: thesis: (diff (sin (#) cos ),Z) . 2 = 4 (#) (((- sin ) (#) cos ) | Z)
A2: cos is_differentiable_on 2,Z by TAYLOR_2:21;
A3: sin is_differentiable_on 2,Z by TAYLOR_2:21;
(diff (sin (#) cos ),Z) . 2 = ((((diff sin ,Z) . (2 * 1)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((diff cos ,Z) . (2 * 1))) by ThB3, A2, A3
.= (((((- 1) |^ 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((diff cos ,Z) . (2 * 1))) by TAYLOR_2:19
.= (((((- 1) |^ 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z))) by TAYLOR_2:19
.= ((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z))) by NEWTON:10
.= ((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((- 1) (#) (cos | Z))) by NEWTON:10
.= ((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((cos | Z) (#) (cos `| Z)))) + (sin (#) ((- 1) (#) (cos | Z))) by TAYLOR_2:17
.= ((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) ((- 1) (#) (cos | Z))) by TAYLOR_2:17
.= (((((- 1) (#) sin ) | Z) (#) cos ) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) ((- 1) (#) (cos | Z))) by RFUNCT_1:65
.= (((((- 1) (#) sin ) | Z) (#) cos ) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) (((- 1) (#) cos ) | Z)) by RFUNCT_1:65
.= ((((- sin ) (#) cos ) | Z) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) ((- cos ) | Z)) by RFUNCT_1:61
.= ((((- sin ) (#) cos ) | Z) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + ((sin (#) (- cos )) | Z) by RFUNCT_1:61
.= ((((- sin ) (#) cos ) | Z) + (2 (#) (((- sin ) (#) cos ) | Z))) + ((sin (#) (- cos )) | Z) by RFUNCT_1:61
.= ((((- sin ) (#) cos ) | Z) + (2 (#) (((- sin ) (#) cos ) | Z))) + (((- 1) (#) (sin (#) cos )) | Z) by RFUNCT_1:25
.= ((((- sin ) (#) cos ) | Z) + (2 (#) (((- sin ) (#) cos ) | Z))) + ((((- 1) (#) sin ) (#) cos ) | Z) by RFUNCT_1:24
.= ((1 (#) (((- sin ) (#) cos ) | Z)) + (2 (#) (((- sin ) (#) cos ) | Z))) + (((- sin ) (#) cos ) | Z) by RFUNCT_1:33
.= ((1 (#) (((- sin ) (#) cos ) | Z)) + (2 (#) (((- sin ) (#) cos ) | Z))) + (1 (#) (((- sin ) (#) cos ) | Z)) by RFUNCT_1:33
.= ((1 + 2) (#) (((- sin ) (#) cos ) | Z)) + (1 (#) (((- sin ) (#) cos ) | Z)) by ThB2
.= (3 + 1) (#) (((- sin ) (#) cos ) | Z) by ThB2
.= 4 (#) (((- sin ) (#) cos ) | Z) ;
hence (diff (sin (#) cos ),Z) . 2 = 4 (#) (((- sin ) (#) cos ) | Z) ; :: thesis: verum