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)) ) )
dom ((- sin) + ((id Z) (#) cos)) = (dom (- sin)) /\ (dom ((id Z) (#) cos)) by VALUED_1:def 1
.= REAL /\ (dom ((id Z) (#) cos)) by SIN_COS:24, VALUED_1:8
.= dom ((id Z) (#) cos) 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 ((- sin) + ((id Z) (#) cos)) by RELAT_1:45;
A2: (id Z) (#) cos is_differentiable_on Z by Th10;
A3: - sin is_differentiable_on Z by FDIFF_1:26, INTEGRA8:24;

now :: thesis: for x being Real st x in Z holds
(((- sin) + ((id Z) (#) cos)) `| Z) . x = - (x * (sin . x))

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:18
.= ((((id Z) (#) cos) `| Z) . x) + (diff ((- sin),x)) by A2, A4, FDIFF_1:def 7
.= ((cos . x) - (x * (sin . x))) + (diff ((- sin),x)) by A4, Th10
.= ((cos . x) - (x * (sin . x))) + (- (cos . x)) by Lm2
.= - (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:18; :: thesis: verum