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

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