let p, r be real number ; :: thesis: tanh . (p + r) = ((tanh . p) + (tanh . r)) / (1 + ((tanh . p) * (tanh . r)))
A1: ( cosh . r <> 0 & cosh . p <> 0 & ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) <> 0 )

proof

((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) = cosh . (p + r) by Lm3;
hence ( cosh . r <> 0 & cosh . p <> 0 & ((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r)) <> 0 ) by Th15; :: thesis: verum

end;

tanh . (p + r) = (sinh . (p + r)) / (cosh . (p + r)) by Th17
.= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (cosh . (p + r)) by Lm4
.= (((sinh . p) * (cosh . r)) + ((cosh . p) * (sinh . r))) / (((cosh . p) * (cosh . r)) + ((sinh . p) * (sinh . r))) by Lm3
.= (((sinh . p) / (cosh . p)) + ((sinh . r) / (cosh . r))) / (1 + (((sinh . p) / (cosh . p)) * ((sinh . r) / (cosh . r)))) by A1, Lm5
.= ((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