theorem :: SIN_COS7:39

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