let p, r be Real; :: thesis: ( (tanh . p) + (tanh . r) = (sinh . (p + r)) / ((cosh . p) * (cosh . r)) & (tanh . p) - (tanh . r) = (sinh . (p - r)) / ((cosh . p) * (cosh . r)) )
A1: (sinh . (p - r)) / ((cosh . p) * (cosh . r)) = (((sinh . p) * (cosh . r)) - ((cosh . p) * (sinh . r))) / ((cosh . p) * (cosh . r)) by Lm8
.= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:120
.= ((sinh . p) / (cosh . p)) - (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by Th15, XCMPLX_1:91
.= ((sinh . p) / (cosh . p)) - ((sinh . r) / (cosh . r)) by Th15, XCMPLX_1:91
.= (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 Lm3
.= (((sinh . p) * (cosh . r)) / ((cosh . p) * (cosh . r))) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by XCMPLX_1:62
.= ((sinh . p) / (cosh . p)) + (((cosh . p) * (sinh . r)) / ((cosh . p) * (cosh . r))) by Th15, XCMPLX_1:91
.= ((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r)) by Th15, XCMPLX_1:91
.= (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 A1; :: thesis: verum