let p, r be Real; :: thesis: tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
A1: ( cosh . r <> 0 & cosh . p <> 0 ) by Th15;
tanh . (p + r) = (sinh . (p + r)) / (cosh . (p + r)) by Th17
.= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (cosh . (p + r)) by Lm3
.= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))) by Lm2
.= (((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by A1, Lm4
.= ((tanh . p) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by Th17
.= ((tanh . p) + (tanh . r)) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by Th17
.= ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * ((sinh . r) / (cosh . r)))) by Th17
.= ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) by Th17 ;
hence tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r))) ; :: thesis: verum