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:61
.= (dom cos) /\ Z by VALUED_1:8
.= dom (cos | Z) by RELAT_1:61
.= 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
.= ((- cos) | Z) . x by RFUNCT_1:49
.= (- cos) . x by A2, FUNCT_1:47 ;
hence ((diff (sin,Z)) . 3) . x = (- cos) . x ; :: thesis: verum