let x be Real; for Z being open Subset of REAL st x in Z holds
((diff (sin,Z)) . 2) . x = - (sin . x)
let Z be open Subset of REAL; ( x in Z implies ((diff (sin,Z)) . 2) . x = - (sin . x) )
assume A1:
x in Z
; ((diff (sin,Z)) . 2) . x = - (sin . x)
A2:
cos is_differentiable_on Z
by FDIFF_1:26, SIN_COS:67;
A3:
sin is_differentiable_on Z
by FDIFF_1:26, SIN_COS:68;
((diff (sin,Z)) . (2 * 1)) . x =
((diff (sin,Z)) . (1 + 1)) . x
.=
(((diff (sin,Z)) . (1 + 0)) `| Z) . x
by TAYLOR_1:def 5
.=
((((diff (sin,Z)) . 0) `| Z) `| Z) . x
by TAYLOR_1:def 5
.=
(((sin | Z) `| Z) `| Z) . x
by TAYLOR_1:def 5
.=
((sin `| Z) `| Z) . x
by A3, FDIFF_2:16
.=
((cos | Z) `| Z) . x
by TAYLOR_2:17
.=
(cos `| Z) . x
by A2, FDIFF_2:16
.=
diff (cos,x)
by A1, A2, FDIFF_1:def 7
.=
- (sin . x)
by SIN_COS:63
;
hence
((diff (sin,Z)) . 2) . x = - (sin . x)
; verum