let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds
integral ((((#Z n) * sin) (#) cos),A) = 0
let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,PI.] implies integral ((((#Z n) * sin) (#) cos),A) = 0 )
assume A = [.0,PI.] ; :: thesis: integral ((((#Z n) * sin) (#) cos),A) = 0
then ( upper_bound A = PI & lower_bound A = 0 ) by INTEGRA8:37;
then integral ((((#Z n) * sin) (#) cos),A) = (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) . PI) - (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) . 0) by Th19
.= ((1 / (n + 1)) * (((#Z (n + 1)) * sin) . PI)) - (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) . 0) by VALUED_1:6
.= ((1 / (n + 1)) * (((#Z (n + 1)) * sin) . PI)) - ((1 / (n + 1)) * (((#Z (n + 1)) * sin) . 0)) by VALUED_1:6
.= ((1 / (n + 1)) * ((#Z (n + 1)) . (sin . pp))) - ((1 / (n + 1)) * (((#Z (n + 1)) * sin) . 0)) by FUNCT_1:13, SIN_COS:24
.= ((1 / (n + 1)) * ((#Z (n + 1)) . (sin . PI))) - ((1 / (n + 1)) * ((#Z (n + 1)) . (sin . 0))) by FUNCT_1:13, SIN_COS:24, Lm6
.= 0 by SIN_COS:30, SIN_COS:76 ;
hence integral ((((#Z n) * sin) (#) cos),A) = 0 ; :: thesis: verum