let Z be open Subset of REAL ; :: thesis: (diff (exp_R (#) cos ),Z) . 2 = 2 (#) ((exp_R (#) (- sin )) | Z)
A2: cos is_differentiable_on 2,Z by TAYLOR_2:21;
A3: exp_R is_differentiable_on 2,Z by TAYLOR_2:10;
A4: dom (0 (#) ((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 ;
A5: dom (2 (#) ((exp_R (#) (- sin )) | Z)) = dom ((exp_R (#) (- sin )) | Z) by VALUED_1:def 5
.= (dom (exp_R (#) (- sin ))) /\ Z by RELAT_1:90
.= ((dom exp_R ) /\ (dom (- sin ))) /\ Z by VALUED_1:def 4
.= (REAL /\ REAL ) /\ Z by SIN_COS:27, SIN_COS:51, VALUED_1:def 5
.= Z by XBOOLE_1:28 ;
A6: dom ((0 (#) ((exp_R (#) cos ) | Z)) + (2 (#) ((exp_R (#) (- sin )) | Z))) = Z /\ Z by A5, A4, VALUED_1:def 1
.= Z ;
A7: exp_R is_differentiable_on Z by FDIFF_1:34, TAYLOR_1:16;
A8: cos is_differentiable_on Z by FDIFF_1:34, SIN_COS:72;
then A9: exp_R (#) cos is_differentiable_on Z by A7, FDIFF_2:20;
exp_R | Z is_differentiable_on Z by A7, FDIFF_2:16;
then A11: (exp_R | Z) (#) cos is_differentiable_on Z by A8, FDIFF_2:20;
sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
then sin | Z is_differentiable_on Z by FDIFF_2:16;
then (- 1) (#) (sin | Z) is_differentiable_on Z by FDIFF_2:19;
then exp_R (#) ((- 1) (#) (sin | Z)) is_differentiable_on Z by A7, FDIFF_2:20;
then A16: ((exp_R | Z) (#) cos ) + (exp_R (#) ((- 1) (#) (sin | Z))) is_differentiable_on Z by A11, FDIFF_2:17;
A17: 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 A9, FDIFF_2:16
.= dom ((((exp_R `| Z) (#) cos ) + (exp_R (#) (cos `| Z))) `| Z) by A7, A8, 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:65
.= Z by A16, FDIFF_1:def 8 ;
for x being 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 Real; :: thesis: ( x in dom ((diff (exp_R (#) cos ),Z) . 2) implies ((diff (exp_R (#) cos ),Z) . 2) . x = (2 (#) ((exp_R (#) (- sin )) | Z)) . x )
assume B1: x in dom ((diff (exp_R (#) cos ),Z) . 2) ; :: thesis: ((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 ThB3, A2, A3
.= ((((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:62
.= ((((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 by NEWTON:10
.= ((((exp_R (#) cos ) | Z) + (2 (#) ((exp_R | Z) (#) (- (sin | Z))))) + (exp_R (#) ((- 1) (#) (cos | Z)))) . x by RFUNCT_1:61
.= ((((exp_R (#) cos ) | Z) + (2 (#) ((exp_R | Z) (#) ((- sin ) | Z)))) + (exp_R (#) ((- 1) (#) (cos | Z)))) . x by RFUNCT_1:62
.= ((((exp_R (#) cos ) | Z) + (2 (#) ((exp_R (#) (- sin )) | Z))) + (exp_R (#) ((- 1) (#) (cos | Z)))) . x by RFUNCT_1:61
.= ((((exp_R (#) cos ) | Z) + (exp_R (#) ((- 1) (#) (cos | Z)))) + (2 (#) ((exp_R (#) (- sin )) | Z))) . x by RFUNCT_1:19
.= ((((exp_R (#) cos ) | Z) + ((- 1) (#) (exp_R (#) (cos | Z)))) + (2 (#) ((exp_R (#) (- sin )) | Z))) . x by RFUNCT_1:25
.= ((((exp_R (#) cos ) | Z) + ((- 1) (#) ((exp_R (#) cos ) | Z))) + (2 (#) ((exp_R (#) (- sin )) | Z))) . x by RFUNCT_1:61
.= (((1 (#) ((exp_R (#) cos ) | Z)) + ((- 1) (#) ((exp_R (#) cos ) | Z))) + (2 (#) ((exp_R (#) (- sin )) | Z))) . x by RFUNCT_1:33
.= (((1 + (- 1)) (#) ((exp_R (#) cos ) | Z)) + (2 (#) ((exp_R (#) (- sin )) | Z))) . x by ThB2
.= ((0 (#) ((exp_R (#) cos ) | Z)) . x) + ((2 (#) ((exp_R (#) (- sin )) | Z)) . x) by A6, B1, A17, VALUED_1:def 1
.= (0 * (((exp_R (#) cos ) | Z) . x)) + ((2 (#) ((exp_R (#) (- sin )) | Z)) . x) by A4, B1, A17, VALUED_1:def 5
.= (2 (#) ((exp_R (#) (- sin )) | Z)) . x ;
hence ((diff (exp_R (#) cos ),Z) . 2) . x = (2 (#) ((exp_R (#) (- sin )) | Z)) . x ; :: thesis: verum

end;

hence (diff (exp_R (#) cos ),Z) . 2 = 2 (#) ((exp_R (#) (- sin )) | Z) by A17, A5, PARTFUN1:34; :: thesis: verum