for p being Real holds
( tanh is_differentiable_in p & diff (tanh,p) = 1 / ((cosh . p) ^2) ) by Lm22, Lm23;