let Z be open Subset of REAL ; :: thesis: ( (- sin ) + ((id Z) (#) cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin ) + ((id Z) (#) cos )) `| Z) . x = - (x * (sin . x)) ) )
A1: Z = dom ((- sin ) + ((id Z) (#) cos ))

proof

dom ((- sin ) + ((id Z) (#) cos )) = (dom (- sin )) /\ (dom ((id Z) (#) cos )) by VALUED_1:def 1
.= REAL /\ (dom ((id Z) (#) cos )) by SIN_COS:27, VALUED_1:8
.= dom ((id Z) (#) cos ) 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 ((- sin ) + ((id Z) (#) cos )) by RELAT_1:71; :: thesis: verum

end;

A2: ( (id Z) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) cos ) `| Z) . x = (cos . x) - (x * (sin . x)) ) ) by Th16;
A3: - sin is_differentiable_on Z by FDIFF_1:34, INTEGRA8:24;

now

let x be Real; :: thesis: ( x in Z implies (((- sin ) + ((id Z) (#) cos )) `| Z) . x = - (x * (sin . x)) )
assume A4: x in Z ; :: thesis: (((- sin ) + ((id Z) (#) cos )) `| Z) . x = - (x * (sin . x))
hence (((- sin ) + ((id Z) (#) cos )) `| Z) . x = (diff (- sin ),x) + (diff ((id Z) (#) cos ),x) by A1, A2, A3, FDIFF_1:26
.= ((((id Z) (#) cos ) `| Z) . x) + (diff (- sin ),x) by A2, A4, FDIFF_1:def 8
.= ((cos . x) - (x * (sin . x))) + (diff (- sin ),x) by A4, Th16
.= ((cos . x) - (x * (sin . x))) + (- (cos . x)) by Lm5
.= - (x * (sin . x)) ;
:: thesis: verum

end;

hence ( (- sin ) + ((id Z) (#) cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- sin ) + ((id Z) (#) cos )) `| Z) . x = - (x * (sin . x)) ) ) by A1, A2, A3, FDIFF_1:26; :: thesis: verum