let x be Real; :: thesis: cosh (x / 2) = sqrt (((cosh x) + 1) / 2)
A1: cosh . (x / 2) > 0 by SIN_COS2:15;
sqrt (((cosh x) + 1) / 2) = sqrt (((cosh . (2 * (x / 2))) + 1) / 2) by SIN_COS2:def 4
.= sqrt ((((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / 2) by SIN_COS2:23
.= cosh . (x / 2) by A1, SQUARE_1:22 ;
hence cosh (x / 2) = sqrt (((cosh x) + 1) / 2) by SIN_COS2:def 4; :: thesis: verum