theorem Th26: :: SIN_COS8:26

for x being Real holds
( sinh (2 * x) = (2 * (sinh x)) * (cosh x) & cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 & tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) )