let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,(2 * PI).] implies integral ((cos ^2),A) = PI )
assume A = [.0,(2 * PI).] ; :: thesis: integral ((cos ^2),A) = PI
then ( upper_bound A = 2 * PI & lower_bound A = 0 ) by INTEGRA8:37;
then integral ((cos ^2),A) = (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (2 * PI)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . 0) by Th16
.= (((AffineMap ((1 / 2),0)) . (2 * PI)) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . dp)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . 0) by VALUED_1:1
.= (((AffineMap ((1 / 2),0)) . (2 * PI)) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . (2 * PI))) - (((AffineMap ((1 / 2),0)) . 0) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by VALUED_1:1, Lm6
.= ((((1 / 2) * (2 * PI)) + 0) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . dp)) - (((AffineMap ((1 / 2),0)) . 0) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by FCONT_1:def 4
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * ((sin * (AffineMap (2,0))) . (2 * PI)))) - (((AffineMap ((1 / 2),0)) . 0) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by VALUED_1:6
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . ((AffineMap (2,0)) . dp)))) - (((AffineMap ((1 / 2),0)) . 0) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by Lm4, FUNCT_1:13
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . ddp))) - (((AffineMap ((1 / 2),0)) . 0) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by FCONT_1:def 4
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . (((2 * 2) * PI) + 0)))) - (0 + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by FCONT_1:48
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . (((2 * 2) * PI) + 0)))) - ((1 / 4) * ((sin * (AffineMap (2,0))) . 0)) by VALUED_1:6
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . (((2 * 2) * PI) + 0)))) - ((1 / 4) * (sin . ((AffineMap (2,0)) . 0))) by Lm4, FUNCT_1:13, Lm6
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . (0 + ((2 * PI) * 2))))) - ((1 / 4) * (sin . 0)) by FCONT_1:48
.= (((1 / 2) * (2 * PI)) + ((1 / 4) * (sin . 0))) - ((1 / 4) * (sin . 0)) by SIN_COS6:8
.= PI ;
hence integral ((cos ^2),A) = PI ; :: thesis: verum