let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds
sin is_orthogonal_with cos ,A
let A be closed-interval Subset of REAL; :: thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies sin is_orthogonal_with cos ,A )
assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; :: thesis: sin is_orthogonal_with cos ,A
then |||(sin,cos,A)||| = 0 by INTEGRA8:95;
hence sin is_orthogonal_with cos ,A by Def2; :: thesis: verum