theorem :: SIN_COS7:34

for x being Real st x < 0 holds
sinh" x = cosh2" (sqrt ((x ^2) + 1))