let x be Real; :: thesis: ( cos . x <> 0 implies ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )
A1: cos is_differentiable_in x by SIN_COS:63;
assume A2: cos . x <> 0 ; :: thesis: ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )
then diff ((cos ^),x) = - ((diff (cos,x)) / ((cos . x) ^2)) by A1, FDIFF_2:15
.= - ((- (sin . x)) / ((cos . x) ^2)) by SIN_COS:63
.= (sin . x) / ((cos . x) ^2) ;
hence ( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) ) by A2, A1, FDIFF_2:15; :: thesis: verum