for x being Real holds cosh (x / 2) = sqrt (((cosh x) + 1) / 2)