theorem :: SIN_COS7:55

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