let p, r be real number ; :: thesis: ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )
A1: ( cosh . p <> 0 & cosh . r <> 0 ) by Th15;
A2: (sinh . (p + r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm4
.= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:63
.= ((sinh . p) / (cosh . p)) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by A1, XCMPLX_1:92
.= ((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r)) by A1, XCMPLX_1:92
.= (tanh . p) + ((sinh . r) / (cosh . r)) by Th17
.= (tanh . p) + (tanh . r) by Th17 ;
(sinh . (p - r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm9
.= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:121
.= ((sinh . p) / (cosh . p)) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by A1, XCMPLX_1:92
.= ((sinh . p) / (cosh . p)) - ((sinh . r) / (cosh . r)) by A1, XCMPLX_1:92
.= (tanh . p) - ((sinh . r) / (cosh . r)) by Th17
.= (tanh . p) - (tanh . r) by Th17 ;
hence ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) ) by A2; :: thesis: verum