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:34, SIN_COS:72;

now

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