theorem Th1: :: SIN_COS8:1

for x being Real holds
( tanh x = (sinh x) / (cosh x) & tanh 0 = 0 )