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