let Z be open Subset of REAL; (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z)
A1:
( sin is_differentiable_on 2,Z & exp_R is_differentiable_on 2,Z )
by TAYLOR_2:10, TAYLOR_2:21;
A2: dom (2 (#) ((exp_R (#) cos) | Z)) =
dom ((exp_R (#) cos) | Z)
by VALUED_1:def 5
.=
(dom (exp_R (#) cos)) /\ Z
by RELAT_1:61
.=
(REAL /\ REAL) /\ Z
by SIN_COS:24, SIN_COS:47, VALUED_1:def 4
.=
Z
by XBOOLE_1:28
;
A3:
exp_R is_differentiable_on Z
by FDIFF_1:26, TAYLOR_1:16;
cos is_differentiable_on Z
by FDIFF_1:26, SIN_COS:67;
then
cos | Z is_differentiable_on Z
by FDIFF_2:16;
then A4:
exp_R (#) (cos | Z) is_differentiable_on Z
by A3, FDIFF_2:20;
A5:
sin is_differentiable_on Z
by FDIFF_1:26, SIN_COS:68;
then A6:
exp_R (#) sin is_differentiable_on Z
by A3, FDIFF_2:20;
exp_R | Z is_differentiable_on Z
by A3, FDIFF_2:16;
then
(exp_R | Z) (#) sin is_differentiable_on Z
by A5, FDIFF_2:20;
then A7:
((exp_R | Z) (#) sin) + (exp_R (#) (cos | Z)) is_differentiable_on Z
by A4, FDIFF_2:17;
A8: dom ((diff ((exp_R (#) sin),Z)) . 2) =
dom ((diff ((exp_R (#) sin),Z)) . (1 + 1))
.=
dom (((diff ((exp_R (#) sin),Z)) . (1 + 0)) `| Z)
by TAYLOR_1:def 5
.=
dom ((((diff ((exp_R (#) sin),Z)) . 0) `| Z) `| Z)
by TAYLOR_1:def 5
.=
dom ((((exp_R (#) sin) | Z) `| Z) `| Z)
by TAYLOR_1:def 5
.=
dom (((exp_R (#) sin) `| Z) `| Z)
by A6, FDIFF_2:16
.=
dom ((((exp_R `| Z) (#) sin) + (exp_R (#) (sin `| Z))) `| Z)
by A3, A5, FDIFF_2:20
.=
dom ((((exp_R | Z) (#) sin) + (exp_R (#) (sin `| Z))) `| Z)
by TAYLOR_2:5
.=
dom ((((exp_R | Z) (#) sin) + (exp_R (#) (cos | Z))) `| Z)
by TAYLOR_2:17
.=
Z
by A7, FDIFF_1:def 7
;
A9: dom (0 (#) ((exp_R (#) sin) | Z)) =
dom ((exp_R (#) sin) | Z)
by VALUED_1:def 5
.=
(dom (exp_R (#) sin)) /\ Z
by RELAT_1:61
.=
(REAL /\ REAL) /\ Z
by SIN_COS:24, SIN_COS:47, VALUED_1:def 4
.=
Z
by XBOOLE_1:28
;
then A10: dom ((0 (#) ((exp_R (#) sin) | Z)) + (2 (#) ((exp_R (#) cos) | Z))) =
Z /\ Z
by A2, VALUED_1:def 1
.=
Z
;
for x being Element of REAL st x in dom ((diff ((exp_R (#) sin),Z)) . 2) holds
((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x
proof
let x be
Element of
REAL ;
( x in dom ((diff ((exp_R (#) sin),Z)) . 2) implies ((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x )
assume A11:
x in dom ((diff ((exp_R (#) sin),Z)) . 2)
;
((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x
((diff ((exp_R (#) sin),Z)) . 2) . x =
(((((diff (exp_R,Z)) . 2) (#) sin) + (2 (#) ((exp_R `| Z) (#) (sin `| Z)))) + (exp_R (#) ((diff (sin,Z)) . 2))) . x
by A1, Th50
.=
((((exp_R | Z) (#) sin) + (2 (#) ((exp_R `| Z) (#) (sin `| Z)))) + (exp_R (#) ((diff (sin,Z)) . 2))) . x
by TAYLOR_2:6
.=
((((exp_R | Z) (#) sin) + (2 (#) ((exp_R | Z) (#) (sin `| Z)))) + (exp_R (#) ((diff (sin,Z)) . 2))) . x
by TAYLOR_2:5
.=
((((exp_R | Z) (#) sin) + (2 (#) ((exp_R | Z) (#) (cos | Z)))) + (exp_R (#) ((diff (sin,Z)) . (2 * 1)))) . x
by TAYLOR_2:17
.=
((((exp_R | Z) (#) sin) + (2 (#) ((exp_R | Z) (#) (cos | Z)))) + (exp_R (#) (((- 1) |^ 1) (#) (sin | Z)))) . x
by TAYLOR_2:19
.=
((((exp_R | Z) (#) sin) + (2 (#) ((exp_R | Z) (#) (cos | Z)))) + (exp_R (#) ((- 1) (#) (sin | Z)))) . x
.=
((((exp_R (#) sin) | Z) + (2 (#) ((exp_R | Z) (#) (cos | Z)))) + (exp_R (#) ((- 1) (#) (sin | Z)))) . x
by RFUNCT_1:45
.=
((((exp_R (#) sin) | Z) + (2 (#) ((exp_R (#) cos) | Z))) + (exp_R (#) ((- 1) (#) (sin | Z)))) . x
by RFUNCT_1:45
.=
((((exp_R (#) sin) | Z) + (exp_R (#) ((- 1) (#) (sin | Z)))) + (2 (#) ((exp_R (#) cos) | Z))) . x
by RFUNCT_1:8
.=
((((exp_R (#) sin) | Z) + ((- 1) (#) (exp_R (#) (sin | Z)))) + (2 (#) ((exp_R (#) cos) | Z))) . x
by RFUNCT_1:13
.=
((((exp_R (#) sin) | Z) + ((- 1) (#) ((exp_R (#) sin) | Z))) + (2 (#) ((exp_R (#) cos) | Z))) . x
by RFUNCT_1:45
.=
(((1 (#) ((exp_R (#) sin) | Z)) + ((- 1) (#) ((exp_R (#) sin) | Z))) + (2 (#) ((exp_R (#) cos) | Z))) . x
by RFUNCT_1:21
.=
(((1 + (- 1)) (#) ((exp_R (#) sin) | Z)) + (2 (#) ((exp_R (#) cos) | Z))) . x
by Th5
.=
((0 (#) ((exp_R (#) sin) | Z)) . x) + ((2 (#) ((exp_R (#) cos) | Z)) . x)
by A10, A8, A11, VALUED_1:def 1
.=
(0 * (((exp_R (#) sin) | Z) . x)) + ((2 (#) ((exp_R (#) cos) | Z)) . x)
by A9, A8, A11, VALUED_1:def 5
.=
(2 (#) ((exp_R (#) cos) | Z)) . x
;
hence
((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x
;
verum
end;
hence
(diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z)
by A2, A8, PARTFUN1:5; verum