let Z be open Subset of REAL; :: thesis: ( Z c= dom sec implies ( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) )
assume Z c= dom sec ; :: thesis: ( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) )
then for x being Real st x in Z holds
cos . x <> 0 by RFUNCT_1:3;
hence ( sec is_differentiable_on Z & ( for x being Real st x in Z holds
(sec `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) by FDIFF_4:39; :: thesis: verum