let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,(PI * 2).] implies sin is_orthogonal_with cos ,A )
assume A1: A = [.0 ,(PI * 2).] ; :: thesis: sin is_orthogonal_with cos ,A
|||(sin ,cos ,A)||| = 0 by A1, INTEGRA8:94;
hence sin is_orthogonal_with cos ,A by Def2; :: thesis: verum