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