let p be Real; :: 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:9; :: thesis: verum