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