let x be Real; :: thesis: 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x)
(cos (x / 2)) ^2 = (1 + (cos (2 * (x / 2)))) / 2 by SIN_COS5:21
.= (1 + (cos x)) / 2 ;
then 2 * ((cos . (x / 2)) ^2) = 2 * ((1 + (cos x)) / 2) by SIN_COS:def 19
.= 1 + (cos . x) by SIN_COS:def 19 ;
hence 2 * ((cos . (x / 2)) ^2) = 1 + (cos . x) ; :: thesis: verum