theorem :: SIN_COS7:50

for x, y being Real st (x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) >= 0 holds
(sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2)))))