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