let p be real number ; :: thesis: ( sinh / cosh is_differentiable_in p & diff (sinh / cosh ),p = 1 / ((cosh . p) ^2 ) )
A1: p is Real by XREAL_0:def 1;
A2: cosh . p <> 0 by Th15;
A3: sinh is_differentiable_in p by Th31;
A4: cosh is_differentiable_in p by Th32;
then diff (sinh / cosh ),p = (((diff sinh ,p) * (cosh . p)) - ((diff cosh ,p) * (sinh . p))) / ((cosh . p) ^2 ) by A1, A2, A3, FDIFF_2:14
.= (((cosh . p) * (cosh . p)) - ((diff cosh ,p) * (sinh . p))) / ((cosh . p) ^2 ) by Th31
.= (((cosh . p) ^2 ) - ((sinh . p) * (sinh . p))) / ((cosh . p) ^2 ) by Th32
.= 1 / ((cosh . p) ^2 ) by Th14 ;
hence ( sinh / cosh is_differentiable_in p & diff (sinh / cosh ),p = 1 / ((cosh . p) ^2 ) ) by A1, A2, A3, A4, FDIFF_2:14; :: thesis: verum