let x be Real; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff cos ,Z) . 2) . x = - (cos . x)
let Z be open Subset of REAL ; :: thesis: ( x in Z implies ((diff cos ,Z) . 2) . x = - (cos . x) )
assume A1: x in Z ; :: thesis: ((diff cos ,Z) . 2) . x = - (cos . x)
A2: cos is_differentiable_on Z by FDIFF_1:34, SIN_COS:72;
dom (((- 1) (#) sin ) | Z) = (dom ((- 1) (#) sin )) /\ Z by RELAT_1:90
.= (dom sin ) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:27, XBOOLE_1:28 ;
then A3: Z c= dom ((- 1) (#) sin ) by RELAT_1:89;
A4: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
then A5: (- 1) (#) sin is_differentiable_on Z by FDIFF_2:19;
((diff cos ,Z) . 2) . x = ((diff cos ,Z) . (1 + 1)) . x
.= (((diff cos ,Z) . (1 + 0 )) `| Z) . x by TAYLOR_1:def 5
.= ((((diff cos ,Z) . 0 ) `| Z) `| Z) . x by TAYLOR_1:def 5
.= (((cos | Z) `| Z) `| Z) . x by TAYLOR_1:def 5
.= ((cos `| Z) `| Z) . x by A2, FDIFF_2:16
.= (((- sin ) | Z) `| Z) . x by TAYLOR_2:17
.= (((- 1) (#) sin ) `| Z) . x by A5, FDIFF_2:16
.= (- 1) * (diff sin ,x) by A1, A4, A3, FDIFF_1:28
.= (- 1) * (cos . x) by SIN_COS:69
.= - (cos . x) ;
hence ((diff cos ,Z) . 2) . x = - (cos . x) ; :: thesis: verum