theorem :: SIN_COS7:52

for x, y being Real st 1 <= x & 1 <= y holds
(cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1))))