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)))
.=
(((exp_R | Z) (#) sin) + ((3 (#) ((exp_R | Z) (#) (cos | Z))) + (3 (#) ((exp_R | Z) (#) ((- 1) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z)))
.=
(((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:45
.=
(((exp_R (#) sin) | Z) + ((3 (#) ((exp_R (#) cos) | Z)) + (3 (#) ((exp_R | Z) (#) ((- 1) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z)))
by RFUNCT_1:45
.=
(((exp_R (#) sin) | Z) + ((3 (#) ((exp_R (#) cos) | Z)) + (3 (#) ((- 1) (#) ((exp_R | Z) (#) (sin | Z)))))) + (exp_R (#) ((- 1) (#) (cos | Z)))
by RFUNCT_1:13
.=
(((exp_R (#) sin) | Z) + ((3 (#) ((exp_R (#) cos) | Z)) + ((3 * (- 1)) (#) ((exp_R | Z) (#) (sin | Z))))) + (exp_R (#) ((- 1) (#) (cos | Z)))
by RFUNCT_1:17
.=
(((exp_R (#) sin) | Z) + ((3 (#) ((exp_R (#) cos) | Z)) + ((- 3) (#) ((exp_R (#) sin) | Z)))) + (exp_R (#) ((- 1) (#) (cos | Z)))
by RFUNCT_1:45
.=
(((exp_R (#) sin) | Z) + ((3 (#) ((exp_R (#) cos) | Z)) + ((- 3) (#) ((exp_R (#) sin) | Z)))) + ((- 1) (#) (exp_R (#) (cos | Z)))
by RFUNCT_1:13
.=
(((exp_R (#) sin) | Z) + ((3 (#) ((exp_R (#) cos) | Z)) + ((- 3) (#) ((exp_R (#) sin) | Z)))) + ((- 1) (#) ((exp_R (#) cos) | Z))
by RFUNCT_1:45
.=
((((exp_R (#) sin) | Z) + (3 (#) ((exp_R (#) cos) | Z))) + ((- 3) (#) ((exp_R (#) sin) | Z))) + ((- 1) (#) ((exp_R (#) cos) | Z))
by RFUNCT_1:8
.=
(((3 (#) ((exp_R (#) cos) | Z)) + (1 (#) ((exp_R (#) sin) | Z))) + ((- 3) (#) ((exp_R (#) sin) | Z))) + ((- 1) (#) ((exp_R (#) cos) | Z))
by RFUNCT_1:21
.=
((3 (#) ((exp_R (#) cos) | Z)) + ((1 (#) ((exp_R (#) sin) | Z)) + ((- 3) (#) ((exp_R (#) sin) | Z)))) + ((- 1) (#) ((exp_R (#) cos) | Z))
by RFUNCT_1:8
.=
((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:8
.=
((- 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:49
.=
(((- 2) (#) (exp_R (#) sin)) | Z) + ((2 (#) (exp_R (#) cos)) | Z)
by RFUNCT_1:49
.=
(((2 * (- 1)) (#) (exp_R (#) sin)) + (2 (#) (exp_R (#) cos))) | Z
by RFUNCT_1:44
.=
((2 (#) ((- 1) (#) (exp_R (#) sin))) + (2 (#) (exp_R (#) cos))) | Z
by RFUNCT_1:17
.=
(2 (#) (((- 1) (#) (exp_R (#) sin)) + (exp_R (#) cos))) | Z
by RFUNCT_1:16
.=
(2 (#) ((exp_R (#) ((- 1) (#) sin)) + (exp_R (#) cos))) | Z
by RFUNCT_1:13
.=
(2 (#) (exp_R (#) ((- sin) + cos))) | Z
by RFUNCT_1:11
;
hence
(diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z
; verum