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:68;
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:68
.= (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