theorem :: SIN_COS7:38

for x being Real st x >= 1 holds
cosh1" x = 2 * (cosh1" (sqrt ((x + 1) / 2)))