theorem :: SIN_COS5:42

for x1, x2 being Real st sinh x1 <> 0 & sinh x2 <> 0 holds
( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) )