theorem :: SIN_COS7:51

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