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