let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.(- (PI / 2)),(PI / 2).] implies sin is_orthogonal_with cos ,A )
assume A = [.(- (PI / 2)),(PI / 2).] ; :: thesis: sin is_orthogonal_with cos ,A
then A1: ( upper_bound A = PI / 2 & lower_bound A = - (PI / 2) ) by INTEGRA8:37;
|||(sin,cos,A)||| = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) by INTEGRA8:90
.= (1 / 2) * (((cos . (PI / 2)) * (cos . (- (PI / 2)))) - ((cos . (PI / 2)) * (cos . (PI / 2)))) by A1, SIN_COS:30
.= (1 / 2) * (((cos . (PI / 2)) * (cos . (PI / 2))) - ((cos . (PI / 2)) * (cos . (PI / 2)))) by SIN_COS:30 ;
hence sin is_orthogonal_with cos ,A ; :: thesis: verum