let Z be open Subset of REAL ; :: thesis:
A2: sin is_differentiable_on 3,Z by TAYLOR_2:21;
A3: exp_R is_differentiable_on 3,Z by TAYLOR_2:10;
(diff (exp_R (#) sin ),Z) . 3 = ((((diff exp_R ,Z) . 3) (#) sin ) + ((3 (#) (((diff exp_R ,Z) . 2) (#) (sin `| Z))) + (3 (#) ((exp_R `| Z) (#) ((diff sin ,Z) . 2))))) + (exp_R (#) ((diff sin ,Z) . 3)) by Th21, A2, A3
.= (((exp_R | Z) (#) sin ) + ((3 (#) (((diff exp_R ,Z) . 2) (#) (sin `| Z))) + (3 (#) ((exp_R `| Z) (#) ((diff sin ,Z) . 2))))) + (exp_R (#) ((diff sin ,Z) . 3)) by TAYLOR_2:6
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (sin `| Z))) + (3 (#) ((exp_R `| Z) (#) ((diff sin ,Z) . 2))))) + (exp_R (#) ((diff sin ,Z) . 3)) by TAYLOR_2:6
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (sin `| Z))) + (3 (#) ((exp_R | Z) (#) ((diff sin ,Z) . 2))))) + (exp_R (#) ((diff sin ,Z) . 3)) by TAYLOR_2:5
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) ((diff sin ,Z) . (2 * 1)))))) + (exp_R (#) ((diff sin ,Z) . ((2 * 1) + 1))) by TAYLOR_2:17
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) (((- 1) |^ 1) (#) (sin | Z)))))) + (exp_R (#) ((diff sin ,Z) . ((2 * 1) + 1))) by TAYLOR_2:19
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) (((- 1) |^ 1) (#) (sin | Z)))))) + (exp_R (#) (((- 1) |^ 1) (#) (cos | Z))) by TAYLOR_2:19
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) ((- 1) (#) (sin | Z)))))) + (exp_R (#) (((- 1) |^ 1) (#) (cos | Z))) by NEWTON:10
.= (((exp_R | Z) (#) sin ) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) ((- 1) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z))) by NEWTON:10
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) ((- 1) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z))) by RFUNCT_1:61
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R (#) cos ) | Z)) + (3 (#) ((exp_R | Z) (#) ((- 1) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z))) by RFUNCT_1:61
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R (#) cos ) | Z)) + (3 (#) ((- 1) (#) ((exp_R | Z) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z))) by RFUNCT_1:25
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R (#) cos ) | Z)) + ((3 * (- 1)) (#) ((exp_R | Z) (#) (sin | Z))))) + (exp_R (#) ((- 1) (#) (cos | Z))) by RFUNCT_1:29
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R (#) cos ) | Z)) + ((- 3) (#) ((exp_R (#) sin ) | Z)))) + (exp_R (#) ((- 1) (#) (cos | Z))) by RFUNCT_1:61
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R (#) cos ) | Z)) + ((- 3) (#) ((exp_R (#) sin ) | Z)))) + ((- 1) (#) (exp_R (#) (cos | Z))) by RFUNCT_1:25
.= (((exp_R (#) sin ) | Z) + ((3 (#) ((exp_R (#) cos ) | Z)) + ((- 3) (#) ((exp_R (#) sin ) | Z)))) + ((- 1) (#) ((exp_R (#) cos ) | Z)) by RFUNCT_1:61
.= ((((exp_R (#) sin ) | Z) + (3 (#) ((exp_R (#) cos ) | Z))) + ((- 3) (#) ((exp_R (#) sin ) | Z))) + ((- 1) (#) ((exp_R (#) cos ) | Z)) by RFUNCT_1:19
.= (((3 (#) ((exp_R (#) cos ) | Z)) + (1 (#) ((exp_R (#) sin ) | Z))) + ((- 3) (#) ((exp_R (#) sin ) | Z))) + ((- 1) (#) ((exp_R (#) cos ) | Z)) by RFUNCT_1:33
.= ((3 (#) ((exp_R (#) cos ) | Z)) + ((1 (#) ((exp_R (#) sin ) | Z)) + ((- 3) (#) ((exp_R (#) sin ) | Z)))) + ((- 1) (#) ((exp_R (#) cos ) | Z)) by RFUNCT_1:19
.= ((3 (#) ((exp_R (#) cos ) | Z)) + ((1 + (- 3)) (#) ((exp_R (#) sin ) | Z))) + ((- 1) (#) ((exp_R (#) cos ) | Z)) by ThB2
.= ((- 2) (#) ((exp_R (#) sin ) | Z)) + ((3 (#) ((exp_R (#) cos ) | Z)) + ((- 1) (#) ((exp_R (#) cos ) | Z))) by RFUNCT_1:19
.= ((- 2) (#) ((exp_R (#) sin ) | Z)) + ((3 + (- 1)) (#) ((exp_R (#) cos ) | Z)) by ThB2
.= (((- 2) (#) (exp_R (#) sin )) | Z) + (2 (#) ((exp_R (#) cos ) | Z)) by RFUNCT_1:65
.= (((- 2) (#) (exp_R (#) sin )) | Z) + ((2 (#) (exp_R (#) cos )) | Z) by RFUNCT_1:65
.= (((2 * (- 1)) (#) (exp_R (#) sin )) + (2 (#) (exp_R (#) cos ))) | Z by RFUNCT_1:60
.= ((2 (#) ((- 1) (#) (exp_R (#) sin ))) + (2 (#) (exp_R (#) cos ))) | Z by RFUNCT_1:29
.= (2 (#) (((- 1) (#) (exp_R (#) sin )) + (exp_R (#) cos ))) | Z by RFUNCT_1:28
.= (2 (#) ((exp_R (#) ((- 1) (#) sin )) + (exp_R (#) cos ))) | Z by RFUNCT_1:25
.= (2 (#) (exp_R (#) ((- sin ) + cos ))) | Z by RFUNCT_1:23 ;
hence (diff (exp_R (#) sin ),Z) . 3 = (2 (#) (exp_R (#) ((- sin ) + cos ))) | Z ; :: thesis: