theorem Th40: :: SIN_COS5:40

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