let Z be open Subset of REAL ; :: thesis: ( Z c= dom (((- (id Z)) (#) cos ) + sin ) implies ( ((- (id Z)) (#) cos ) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos ) + sin ) `| Z) . x = x * (sin . x) ) ) )
assume A1: Z c= dom (((- (id Z)) (#) cos ) + sin ) ; :: thesis: ( ((- (id Z)) (#) cos ) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos ) + sin ) `| Z) . x = x * (sin . x) ) )
then Z c= (dom ((- (id Z)) (#) cos )) /\ (dom sin ) by VALUED_1:def 1;
then A2: ( Z c= dom ((- (id Z)) (#) cos ) & Z c= dom sin ) by XBOOLE_1:18;
then A3: ( (- (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 Th44;
A4: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;

now

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

end;

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