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) by XBOOLE_1:18;
then A3: (- (id Z)) (#) cos is_differentiable_on Z by Th44;
A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;

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

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