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