let x be Real; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff sin ,Z) . 3) . x = (- cos ) . x
let Z be open Subset of REAL ; :: thesis: ( x in Z implies ((diff sin ,Z) . 3) . x = (- cos ) . x )
assume x in Z ; :: thesis: ((diff sin ,Z) . 3) . x = (- cos ) . x
then A1: x in dom (cos | Z) by TAYLOR_2:17;
dom ((- cos ) | Z) = (dom (- cos )) /\ Z by RELAT_1:90
.= (dom cos ) /\ Z by VALUED_1:8
.= dom (cos | Z) by RELAT_1:90
.= dom (- (cos | Z)) by VALUED_1:8 ;
then A2: x in dom ((- cos ) | Z) by A1, VALUED_1:8;
((diff sin ,Z) . 3) . x = ((diff sin ,Z) . ((2 * 1) + 1)) . x
.= (((- 1) |^ 1) (#) (cos | Z)) . x by TAYLOR_2:19
.= ((- 1) (#) (cos | Z)) . x by NEWTON:10
.= ((- cos ) | Z) . x by RFUNCT_1:65
.= (- cos ) . x by A2, FUNCT_1:70 ;
hence ((diff sin ,Z) . 3) . x = (- cos ) . x ; :: thesis: verum