let p be real number ; :: thesis: tanh . p = (sinh . p) / (cosh . p)
(sinh . p) / (cosh . p) = (((exp_R . p) - (exp_R . (- p))) / 2) / (cosh . p) by Def1
.= (((exp_R . p) - (exp_R . (- p))) / 2) / (((exp_R . p) + (exp_R . (- p))) / 2) by Def3
.= ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) by XCMPLX_1:55
.= tanh . p by Def5 ;
hence tanh . p = (sinh . p) / (cosh . p) ; :: thesis: verum