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