let p be Real; ( sinh / cosh is_differentiable_in p & diff ((sinh / cosh),p) = 1 / ((cosh . p) ^2) )
A1:
( p is Real & cosh . p <> 0 )
by Th15;
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