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:34, SIN_COS:72;
A3: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
((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 A2, A1, FDIFF_1:def 8
.= - (sin . x) by SIN_COS:68 ;
hence ((diff sin ,Z) . 2) . x = - (sin . x) ; :: thesis: verum