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