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