let Z be open Subset of REAL ; (diff (sin (#) cos ),Z) . 2 = 4 (#) (((- sin ) (#) cos ) | Z)
( cos is_differentiable_on 2,Z & sin is_differentiable_on 2,Z )
by TAYLOR_2:21;
then (diff (sin (#) cos ),Z) . 2 =
((((diff sin ,Z) . (2 * 1)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((diff cos ,Z) . (2 * 1)))
by Th50
.=
(((((- 1) |^ 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((diff cos ,Z) . (2 * 1)))
by TAYLOR_2:19
.=
(((((- 1) |^ 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
by TAYLOR_2:19
.=
((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
by NEWTON:10
.=
((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((- 1) (#) (cos | Z)))
by NEWTON:10
.=
((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((cos | Z) (#) (cos `| Z)))) + (sin (#) ((- 1) (#) (cos | Z)))
by TAYLOR_2:17
.=
((((- 1) (#) (sin | Z)) (#) cos ) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) ((- 1) (#) (cos | Z)))
by TAYLOR_2:17
.=
(((((- 1) (#) sin ) | Z) (#) cos ) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) ((- 1) (#) (cos | Z)))
by RFUNCT_1:65
.=
(((((- 1) (#) sin ) | Z) (#) cos ) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) (((- 1) (#) cos ) | Z))
by RFUNCT_1:65
.=
((((- sin ) (#) cos ) | Z) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + (sin (#) ((- cos ) | Z))
by RFUNCT_1:61
.=
((((- sin ) (#) cos ) | Z) + (2 (#) ((cos | Z) (#) ((- sin ) | Z)))) + ((sin (#) (- cos )) | Z)
by RFUNCT_1:61
.=
((((- sin ) (#) cos ) | Z) + (2 (#) (((- sin ) (#) cos ) | Z))) + ((sin (#) (- cos )) | Z)
by RFUNCT_1:61
.=
((((- sin ) (#) cos ) | Z) + (2 (#) (((- sin ) (#) cos ) | Z))) + (((- 1) (#) (sin (#) cos )) | Z)
by RFUNCT_1:25
.=
((((- sin ) (#) cos ) | Z) + (2 (#) (((- sin ) (#) cos ) | Z))) + ((((- 1) (#) sin ) (#) cos ) | Z)
by RFUNCT_1:24
.=
((1 (#) (((- sin ) (#) cos ) | Z)) + (2 (#) (((- sin ) (#) cos ) | Z))) + (((- sin ) (#) cos ) | Z)
by RFUNCT_1:33
.=
((1 (#) (((- sin ) (#) cos ) | Z)) + (2 (#) (((- sin ) (#) cos ) | Z))) + (1 (#) (((- sin ) (#) cos ) | Z))
by RFUNCT_1:33
.=
((1 + 2) (#) (((- sin ) (#) cos ) | Z)) + (1 (#) (((- sin ) (#) cos ) | Z))
by Th5
.=
(3 + 1) (#) (((- sin ) (#) cos ) | Z)
by Th5
.=
4 (#) (((- sin ) (#) cos ) | Z)
;
hence
(diff (sin (#) cos ),Z) . 2 = 4 (#) (((- sin ) (#) cos ) | Z)
; verum