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 A1: x in Z ; :: thesis: ((diff cos ,Z) . 3) . x = sin . x
A2: x in dom (sin | Z) by A1, 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:2
.= ((1 * 1) (#) (sin | Z)) . x by WSIERP_1:2
.= (sin | Z) . x by RFUNCT_1:33
.= sin . x by A2, FUNCT_1:70 ;
hence ((diff cos ,Z) . 3) . x = sin . x ; :: thesis: verum