let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,(2 * PI ).] implies integral (sin ^2 ),A = PI )
assume A = [.0 ,(2 * PI ).] ; :: thesis: integral (sin ^2 ),A = PI
then ( upper_bound A = 2 * PI & lower_bound A = 0 ) by INTEGRA8:37;
then integral (sin ^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 Th13
.= (((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 Lm5, VALUED_1:13
.= (((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 Lm5, VALUED_1:13
.= ((((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 Lm4, 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 )))) - 0 ) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )
.= (((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: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 (sin ^2 ),A = PI ; :: thesis: verum