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:72
.= ((sin . x) #R (1 + 1)) #R (1 / 2) by A1, PREPOWER:91
.= (((sin . x) #R 1) * ((sin . x) #R 1)) #R (1 / 2) by A1, PREPOWER:75
.= ((sin . x) * ((sin . x) #R 1)) #R (1 / 2) by A1, PREPOWER:72
.= ((((sin . x) ^2) + ((cos . x) ^2)) - ((cos . x) ^2)) #R (1 / 2) by A1, PREPOWER:72
.= ((1 ^2) - ((cos . x) ^2)) #R (1 / 2) by SIN_COS:28
.= ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2) ;
hence sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2) ; :: thesis: verum