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