let x be Real; :: thesis: ( sin . x > 0 implies sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2) )
assume A1: sin . x > 0 ; :: thesis: sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2)
then sin . x = (sin . x) #R (2 * (1 / 2)) by PREPOWER:86
.= ((sin . x) #R (1 + 1)) #R (1 / 2) by A1, PREPOWER:105
.= (((sin . x) #R 1) * ((sin . x) #R 1)) #R (1 / 2) by A1, PREPOWER:89
.= ((sin . x) * ((sin . x) #R 1)) #R (1 / 2) by A1, PREPOWER:86
.= ((((sin . x) ^2 ) + ((cos . x) ^2 )) - ((cos . x) ^2 )) #R (1 / 2) by A1, PREPOWER:86
.= ((1 ^2 ) - ((cos . x) ^2 )) #R (1 / 2) by SIN_COS:31
.= ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2) ;
hence sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2) ; :: thesis: verum