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