let p, r be Real; :: thesis: tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r)))
tanh . (p - r) = tanh . (p + (- r))
.= ((tanh . p) + (tanh . (- r))) / (1 + ((tanh . p) * (tanh . (- r)))) by Lm5
.= ((tanh . p) + (- (tanh . r))) / (1 + ((tanh . p) * (tanh . (- r)))) by Th19
.= ((tanh . p) - (tanh . r)) / (1 + ((tanh . p) * (- (tanh . r)))) by Th19
.= ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ;
hence tanh . (p - r) = ((tanh . p) - (tanh . r)) / (1 - ((tanh . p) * (tanh . r))) ; :: thesis: verum