let Z be open Subset of REAL ; (diff (exp_R (#) sin ),Z) . 3 = (2 (#) (exp_R (#) ((- sin ) + cos ))) | Z
( sin is_differentiable_on 3,Z & exp_R is_differentiable_on 3,Z )
by TAYLOR_2:10, TAYLOR_2:21;
then (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 Th64
.=
(((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 Th5
.=
((- 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 Th5
.=
(((- 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
; verum