let th be Real; :: thesis: (sin th) * (sin th) = 1 - ((cos th) * (cos th))
(sin th) * (sin th) = ((sin th) * (sin th)) + (1 - 1)
.= ((sin th) * (sin th)) + (1 - (- (- (((sin th) * (sin th)) + ((cos th) * (cos th)))))) by SIN_COS:29
.= 1 - ((cos th) * (cos th)) ;
hence (sin th) * (sin th) = 1 - ((cos th) * (cos th)) ; :: thesis: verum