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:13;
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