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:26, SIN_COS:67;
dom (((- 1) (#) sin) | Z) = (dom ((- 1) (#) sin)) /\ Z by RELAT_1:61
.= (dom sin) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24, XBOOLE_1:28 ;
then A3: Z c= dom ((- 1) (#) sin) by RELAT_1:60;
A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
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:20
.= (- 1) * (cos . x) by SIN_COS:64
.= - (cos . x) ;
hence ((diff (cos,Z)) . 2) . x = - (cos . x) ; :: thesis: verum