let A be 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 B: ( sup A = 2 * PI & inf A = 0 ) by INTEGRA8:37;
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 B, Th16
.= (((AffineMap (1 / 2),0 ) . (2 * PI )) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . (2 * PI ))) - (((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
.= ((((1 / 2) * (2 * PI )) + 0 ) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . (2 * PI ))) - (((AffineMap (1 / 2),0 ) . 0 ) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by JORDAN16:def 3
.= (((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 ) . (2 * PI ))))) - (((AffineMap (1 / 2),0 ) . 0 ) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by C, FUNCT_1:23
.= (((1 / 2) * (2 * PI )) + ((1 / 4) * (sin . ((2 * (2 * PI )) + 0 )))) - (((AffineMap (1 / 2),0 ) . 0 ) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by JORDAN16:def 3
.= (((1 / 2) * (2 * PI )) + ((1 / 4) * (sin . (((2 * 2) * PI ) + 0 )))) - (0 + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by JORDAN16:25
.= (((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 C, FUNCT_1:23
.= (((1 / 2) * (2 * PI )) + ((1 / 4) * (sin . (0 + ((2 * PI ) * 2))))) - ((1 / 4) * (sin . 0 )) by JORDAN16:25
.= (((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