let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL st A = [.0 ,(2 * PI ).] holds
integral (((#Z n) * sin ) (#) cos ),A = 0
let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,(2 * PI ).] implies integral (((#Z n) * sin ) (#) cos ),A = 0 )
assume A = [.0 ,(2 * PI ).] ; :: thesis: integral (((#Z n) * sin ) (#) cos ),A = 0
then B: ( sup A = 2 * PI & inf A = 0 ) by INTEGRA8:37;
integral (((#Z n) * sin ) (#) cos ),A = (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin )) . (2 * PI )) - (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin )) . 0 ) by B, Th19
.= ((1 / (n + 1)) * (((#Z (n + 1)) * sin ) . (2 * PI ))) - (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin )) . 0 ) by VALUED_1:6
.= ((1 / (n + 1)) * (((#Z (n + 1)) * sin ) . (2 * PI ))) - ((1 / (n + 1)) * (((#Z (n + 1)) * sin ) . 0 )) by VALUED_1:6
.= ((1 / (n + 1)) * ((#Z (n + 1)) . (sin . (2 * PI )))) - ((1 / (n + 1)) * (((#Z (n + 1)) * sin ) . 0 )) by SIN_COS:27, FUNCT_1:23
.= ((1 / (n + 1)) * ((#Z (n + 1)) . (sin . (2 * PI )))) - ((1 / (n + 1)) * ((#Z (n + 1)) . (sin . 0 ))) by SIN_COS:27, FUNCT_1:23
.= 0 by SIN_COS:81, SIN_COS:33 ;
hence integral (((#Z n) * sin ) (#) cos ),A = 0 ; :: thesis: verum