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 Lm23, Lm24;
hence ( tanh is_differentiable_on REAL & diff tanh ,p = 1 / ((cosh . p) ^2 ) ) by Lm23, Lm24, Th30, FDIFF_1:16; :: thesis: verum