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)))
.=
((((- 1) (#) (sin | Z)) (#) cos) + (2 (#) ((sin `| Z) (#) (cos `| Z)))) + (sin (#) ((- 1) (#) (cos | Z)))
.=
((((- 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:49
.=
(((((- 1) (#) sin) | Z) (#) cos) + (2 (#) ((cos | Z) (#) ((- sin) | Z)))) + (sin (#) (((- 1) (#) cos) | Z))
by RFUNCT_1:49
.=
((((- sin) (#) cos) | Z) + (2 (#) ((cos | Z) (#) ((- sin) | Z)))) + (sin (#) ((- cos) | Z))
by RFUNCT_1:45
.=
((((- sin) (#) cos) | Z) + (2 (#) ((cos | Z) (#) ((- sin) | Z)))) + ((sin (#) (- cos)) | Z)
by RFUNCT_1:45
.=
((((- sin) (#) cos) | Z) + (2 (#) (((- sin) (#) cos) | Z))) + ((sin (#) (- cos)) | Z)
by RFUNCT_1:45
.=
((((- sin) (#) cos) | Z) + (2 (#) (((- sin) (#) cos) | Z))) + (((- 1) (#) (sin (#) cos)) | Z)
by RFUNCT_1:13
.=
((((- sin) (#) cos) | Z) + (2 (#) (((- sin) (#) cos) | Z))) + ((((- 1) (#) sin) (#) cos) | Z)
by RFUNCT_1:12
.=
((1 (#) (((- sin) (#) cos) | Z)) + (2 (#) (((- sin) (#) cos) | Z))) + (((- sin) (#) cos) | Z)
by RFUNCT_1:21
.=
((1 (#) (((- sin) (#) cos) | Z)) + (2 (#) (((- sin) (#) cos) | Z))) + (1 (#) (((- sin) (#) cos) | Z))
by RFUNCT_1:21
.=
((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