let Z be open Subset of REAL; :: thesis: ( Z c= dom (((id Z) (#) sin) + cos) implies ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) ) )
assume A1: Z c= dom (((id Z) (#) sin) + cos) ; :: thesis: ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) )
then Z c= (dom ((id Z) (#) sin)) /\ (dom cos) by VALUED_1:def 1;
then A2: Z c= dom ((id Z) (#) sin) by XBOOLE_1:18;
then A3: (id Z) (#) sin is_differentiable_on Z by Th45;
A4: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67;

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

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

end;

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