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)) ) )
A1: Z = dom ((- cos ) - ((id Z) (#) sin ))

proof

dom ((- cos ) - ((id Z) (#) sin )) = (dom (- cos )) /\ (dom ((id Z) (#) sin )) by VALUED_1:12
.= REAL /\ (dom ((id Z) (#) sin )) by SIN_COS:27, VALUED_1:8
.= dom ((id Z) (#) sin ) by XBOOLE_1:28
.= (dom (id Z)) /\ REAL by SIN_COS:27, VALUED_1:def 4
.= dom (id Z) by XBOOLE_1:28 ;
hence Z = dom ((- cos ) - ((id Z) (#) sin )) by RELAT_1:71; :: thesis: verum

end;

then Z c= (dom (- cos )) /\ (dom ((id Z) (#) sin )) by VALUED_1:12;
then A2: ( Z c= dom ((id Z) (#) sin ) & Z c= dom (- cos ) ) by XBOOLE_1:18;
then A3: ( (id Z) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) sin ) `| Z) . x = (sin . x) + (x * (cos . x)) ) ) by FDIFF_4:45;
A4: - cos is_differentiable_on Z by FDIFF_1:34, INTEGRA8:26;

now

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:27
.= (sin . x) - (diff ((id Z) (#) sin ),x) by INTEGRA8:26
.= (sin . x) - ((((id Z) (#) sin ) `| Z) . x) by A3, A5, FDIFF_1:def 8
.= (sin . x) - ((sin . x) + (x * (cos . x))) by A5, A2, 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:27; :: thesis: verum