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:90
.=
(REAL /\ REAL ) /\ Z
by SIN_COS:27, SIN_COS:51, VALUED_1:def 4
.=
Z
by XBOOLE_1:28
;
A3:
exp_R is_differentiable_on Z
by FDIFF_1:34, TAYLOR_1:16;
cos is_differentiable_on Z
by FDIFF_1:34, SIN_COS:72;
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:34, SIN_COS:73;
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 8
;
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:90
.=
(REAL /\ REAL ) /\ Z
by SIN_COS:27, SIN_COS:51, 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 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
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
by NEWTON:10
.=
((((exp_R (#) sin ) | Z) + (2 (#) ((exp_R | Z) (#) (cos | Z)))) + (exp_R (#) ((- 1) (#) (sin | Z)))) . x
by RFUNCT_1:61
.=
((((exp_R (#) sin ) | Z) + (2 (#) ((exp_R (#) cos ) | Z))) + (exp_R (#) ((- 1) (#) (sin | Z)))) . x
by RFUNCT_1:61
.=
((((exp_R (#) sin ) | Z) + (exp_R (#) ((- 1) (#) (sin | Z)))) + (2 (#) ((exp_R (#) cos ) | Z))) . x
by RFUNCT_1:19
.=
((((exp_R (#) sin ) | Z) + ((- 1) (#) (exp_R (#) (sin | Z)))) + (2 (#) ((exp_R (#) cos ) | Z))) . x
by RFUNCT_1:25
.=
((((exp_R (#) sin ) | Z) + ((- 1) (#) ((exp_R (#) sin ) | Z))) + (2 (#) ((exp_R (#) cos ) | Z))) . x
by RFUNCT_1:61
.=
(((1 (#) ((exp_R (#) sin ) | Z)) + ((- 1) (#) ((exp_R (#) sin ) | Z))) + (2 (#) ((exp_R (#) cos ) | Z))) . x
by RFUNCT_1:33
.=
(((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:34; verum