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