let x be Real; :: thesis: ( x >= 0 implies sinh (x / 2) = sqrt (((cosh x) - 1) / 2) )
assume x >= 0 ; :: thesis: sinh (x / 2) = sqrt (((cosh x) - 1) / 2)
then sinh (x / 2) = sqrt ((sinh (x / 2)) ^2) by SIN_COS5:46, SQUARE_1:22
.= sqrt ((sinh . (x / 2)) ^2) by SIN_COS2:def 2
.= sqrt ((1 / 2) * ((cosh . (2 * (x / 2))) - 1)) by SIN_COS2:18
.= sqrt (((cosh . x) - 1) / 2)
.= sqrt (((cosh x) - 1) / 2) by SIN_COS2:def 4 ;
hence sinh (x / 2) = sqrt (((cosh x) - 1) / 2) ; :: thesis: verum