let A be closed-interval Subset of REAL ; :: thesis: ( A = [.(- PI ),PI .] implies sin is_orthogonal_with cos ,A )
assume A = [.(- PI ),PI .] ; :: thesis: sin is_orthogonal_with cos ,A
then A1: ( sup A = PI & inf A = - PI ) by INTEGRA8:37;
|||(sin ,cos ,A)||| = (1 / 2) * (((cos . (inf A)) * (cos . (inf A))) - ((cos . (sup A)) * (cos . (sup A)))) by INTEGRA8:90
.= (1 / 2) * (((cos . PI ) * (cos . (- PI ))) - ((cos . PI ) * (cos . PI ))) by A1, SIN_COS:33
.= (1 / 2) * (((cos . PI ) * (cos . PI )) - ((cos . PI ) * (cos . PI ))) by SIN_COS:33 ;
hence sin is_orthogonal_with cos ,A by Def2; :: thesis: verum