theorem :: SIN_COS7:40

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