let Z be open Subset of REAL; (diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z)
sin is_differentiable_on 3,Z
by TAYLOR_2:21;
then (diff ((sin (#) sin),Z)) . 3 =
((((diff (sin,Z)) . ((2 * 1) + 1)) (#) sin) + ((3 (#) (((diff (sin,Z)) . (2 * 1)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) ((diff (sin,Z)) . (2 * 1)))))) + (sin (#) ((diff (sin,Z)) . ((2 * 1) + 1)))
by Th64
.=
(((((- 1) |^ 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((diff (sin,Z)) . (2 * 1)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) ((diff (sin,Z)) . (2 * 1)))))) + (sin (#) ((diff (sin,Z)) . ((2 * 1) + 1)))
by TAYLOR_2:19
.=
(((((- 1) |^ 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((diff (sin,Z)) . (2 * 1)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) ((diff (sin,Z)) . (2 * 1)))))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
by TAYLOR_2:19
.=
(((((- 1) |^ 1) (#) (cos | Z)) (#) sin) + ((3 (#) ((((- 1) |^ 1) (#) (sin | Z)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) ((diff (sin,Z)) . (2 * 1)))))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
by TAYLOR_2:19
.=
(((((- 1) |^ 1) (#) (cos | Z)) (#) sin) + ((3 (#) ((((- 1) |^ 1) (#) (sin | Z)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) (((- 1) |^ 1) (#) (sin | Z)))))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
by TAYLOR_2:19
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 (#) ((((- 1) |^ 1) (#) (sin | Z)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) (((- 1) |^ 1) (#) (sin | Z)))))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((- 1) (#) (sin | Z)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) (((- 1) |^ 1) (#) (sin | Z)))))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((- 1) (#) (sin | Z)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) ((- 1) (#) (sin | Z)))))) + (sin (#) (((- 1) |^ 1) (#) (cos | Z)))
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((- 1) (#) (sin | Z)) (#) (sin `| Z))) + (3 (#) ((sin `| Z) (#) ((- 1) (#) (sin | Z)))))) + (sin (#) ((- 1) (#) (cos | Z)))
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((- 1) (#) (sin | Z)) (#) (cos | Z))) + (3 (#) ((sin `| Z) (#) ((- 1) (#) (sin | Z)))))) + (sin (#) ((- 1) (#) (cos | Z)))
by TAYLOR_2:17
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 (#) (((- 1) (#) (sin | Z)) (#) (cos | Z))) + (3 (#) ((cos | Z) (#) ((- 1) (#) (sin | Z)))))) + (sin (#) ((- 1) (#) (cos | Z)))
by TAYLOR_2:17
.=
((((- 1) (#) (cos | Z)) (#) sin) + ((3 + 3) (#) ((cos | Z) (#) ((- 1) (#) (sin | Z))))) + (sin (#) ((- 1) (#) (cos | Z)))
by Th5
.=
(6 (#) ((cos | Z) (#) ((- 1) (#) (sin | Z)))) + ((((- 1) (#) (cos | Z)) (#) sin) + (((- 1) (#) (cos | Z)) (#) sin))
by RFUNCT_1:8
.=
(6 (#) ((cos | Z) (#) ((- 1) (#) (sin | Z)))) + ((1 (#) (((- 1) (#) (cos | Z)) (#) sin)) + (((- 1) (#) (cos | Z)) (#) sin))
by RFUNCT_1:21
.=
(6 (#) ((cos | Z) (#) ((- 1) (#) (sin | Z)))) + ((1 (#) (((- 1) (#) (cos | Z)) (#) sin)) + (1 (#) (((- 1) (#) (cos | Z)) (#) sin)))
by RFUNCT_1:21
.=
(6 (#) ((cos | Z) (#) ((- 1) (#) (sin | Z)))) + ((1 + 1) (#) (((- 1) (#) (cos | Z)) (#) sin))
by Th5
.=
(6 (#) ((- 1) (#) ((cos | Z) (#) (sin | Z)))) + (2 (#) (((- 1) (#) (cos | Z)) (#) sin))
by RFUNCT_1:13
.=
(6 (#) ((- 1) (#) ((cos (#) sin) | Z))) + (2 (#) (((- 1) (#) (cos | Z)) (#) sin))
by RFUNCT_1:45
.=
(6 (#) ((- 1) (#) ((cos (#) sin) | Z))) + (2 (#) ((- 1) (#) ((cos | Z) (#) sin)))
by RFUNCT_1:12
.=
(6 (#) ((- 1) (#) ((cos (#) sin) | Z))) + (2 (#) ((- 1) (#) ((cos (#) sin) | Z)))
by RFUNCT_1:45
.=
(6 + 2) (#) ((- 1) (#) ((cos (#) sin) | Z))
by Th5
.=
(8 * (- 1)) (#) ((cos (#) sin) | Z)
by RFUNCT_1:17
.=
(- 8) (#) ((cos (#) sin) | Z)
;
hence
(diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z)
; verum