theorem :: SIN_COS8:18

for y, z being Real holds
( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) )