let x be Real; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . 2) . x = - (sin . x)
let Z be open Subset of REAL; :: thesis: ( x in Z implies ((diff (sin,Z)) . 2) . x = - (sin . x) )
assume A1: x in Z ; :: thesis: ((diff (sin,Z)) . 2) . x = - (sin . x)
A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;
A3: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
((diff (sin,Z)) . (2 * 1)) . x = ((diff (sin,Z)) . (1 + 1)) . x
.= (((diff (sin,Z)) . (1 + 0)) `| Z) . x by TAYLOR_1:def 5
.= ((((diff (sin,Z)) . 0) `| Z) `| Z) . x by TAYLOR_1:def 5
.= (((sin | Z) `| Z) `| Z) . x by TAYLOR_1:def 5
.= ((sin `| Z) `| Z) . x by A3, FDIFF_2:16
.= ((cos | Z) `| Z) . x by TAYLOR_2:17
.= (cos `| Z) . x by A2, FDIFF_2:16
.= diff (cos,x) by A1, A2, FDIFF_1:def 7
.= - (sin . x) by SIN_COS:63 ;
hence ((diff (sin,Z)) . 2) . x = - (sin . x) ; :: thesis: verum