for p being Real holds
( tanh is_differentiable_on REAL & diff (tanh,p) = 1 / ((cosh . p) ^2) )