let p be real number ; :: thesis: ( tanh is_differentiable_on REAL & diff tanh ,p = 1 / ((cosh . p) ^2 ) )
( [#] REAL is open Subset of REAL & ( for p being Real st p in REAL holds
tanh is_differentiable_in p ) ) by Lm22, Lm23;
hence ( tanh is_differentiable_on REAL & diff tanh ,p = 1 / ((cosh . p) ^2 ) ) by Lm22, Lm23, Th30, FDIFF_1:16; :: thesis: verum