let x be Real; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff (cos,Z)) . 3) . x = sin . x
let Z be open Subset of REAL; :: thesis: ( x in Z implies ((diff (cos,Z)) . 3) . x = sin . x )
assume x in Z ; :: thesis: ((diff (cos,Z)) . 3) . x = sin . x
then A1: x in dom (sin | Z) by TAYLOR_2:17;
((diff (cos,Z)) . 3) . x = ((diff (cos,Z)) . ((2 * 1) + 1)) . x
.= (((- 1) |^ (1 + 1)) (#) (sin | Z)) . x by TAYLOR_2:19
.= ((1 |^ 2) (#) (sin | Z)) . x by WSIERP_1:1
.= ((1 * 1) (#) (sin | Z)) . x
.= (sin | Z) . x by RFUNCT_1:21
.= sin . x by A1, FUNCT_1:47 ;
hence ((diff (cos,Z)) . 3) . x = sin . x ; :: thesis: verum