let Z be open Subset of REAL; :: thesis: ( (- 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 :: thesis: for x being Real st x in Z holds
(((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x))

let x be Real; :: thesis: ( x in Z implies (((- cos) - ((id Z) (#) sin)) `| Z) . x = - (x * (cos . x)) )
assume A5: x in Z ; :: thesis: (((- 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)) ;
:: thesis: 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; :: thesis: verum