let Z be open Subset of REAL; ( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) )
dom ((- cos) - ((id Z) (#) sin)) =
(dom (- cos)) /\ (dom ((id Z) (#) sin))
by VALUED_1:12
.=
REAL /\ (dom ((id Z) (#) sin))
by SIN_COS:24, VALUED_1:8
.=
dom ((id Z) (#) sin)
by XBOOLE_1:28
.=
(dom (id Z)) /\ REAL
by SIN_COS:24, VALUED_1:def 4
.=
dom (id Z)
by XBOOLE_1:28
;
then A1:
Z = dom ((- cos) - ((id Z) (#) sin))
by RELAT_1:45;
then
Z c= (dom (- cos)) /\ (dom ((id Z) (#) sin))
by VALUED_1:12;
then A2:
Z c= dom ((id Z) (#) sin)
by XBOOLE_1:18;
then A3:
(id Z) (#) sin is_differentiable_on Z
by FDIFF_4:45;
A4:
- cos is_differentiable_on Z
by FDIFF_1:26, INTEGRA8:26;
now for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x))let x be
Real;
( x in Z implies (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) )assume A5:
x in Z
;
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x))hence (((- cos) - ((id Z) (#) sin)) `| Z) . x =
(diff ((- cos),x)) - (diff (((id Z) (#) sin),x))
by A1, A3, A4, FDIFF_1:19
.=
(sin . x) - (diff (((id Z) (#) sin),x))
by INTEGRA8:26, A5
.=
(sin . x) - ((((id Z) (#) sin) `| Z) . x)
by A3, A5, FDIFF_1:def 7
.=
(sin . x) - ((sin . x) + (x * (cos . x)))
by A2, A5, FDIFF_4:45
.=
- (x * (cos . x))
;
verum end;
hence
( (- cos) - ((id Z) (#) sin) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) ) )
by A1, A3, A4, FDIFF_1:19; verum