let x be Real; :: thesis: ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) )
A1: sin is_differentiable_in x by SIN_COS:64;
then diff ((- sin),x) = - (diff (sin,x)) by INTEGRA8:22
.= - (cos . x) by SIN_COS:64 ;
hence ( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) ) by A1, INTEGRA8:22; :: thesis: verum