let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,PI .] implies integral (sin ^2 ),A = PI / 2 )
assume A = [.0 ,PI .] ; :: thesis: integral (sin ^2 ),A = PI / 2
then B: ( sup A = PI & inf A = 0 ) by INTEGRA8:37;
integral (sin ^2 ),A = (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . PI ) - (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . 0 ) by B, Th13
.= (((AffineMap (1 / 2),0 ) . PI ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . PI )) - (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . 0 ) by C, VALUED_1:13
.= (((AffineMap (1 / 2),0 ) . PI ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . PI )) - (((AffineMap (1 / 2),0 ) . 0 ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by C, VALUED_1:13
.= ((((1 / 2) * PI ) + 0 ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . PI )) - (((AffineMap (1 / 2),0 ) . 0 ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by JORDAN16:def 3
.= (((1 / 2) * PI ) - ((1 / 4) * ((sin * (AffineMap 2,0 )) . PI ))) - (((AffineMap (1 / 2),0 ) . 0 ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by VALUED_1:6
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . ((AffineMap 2,0 ) . PI )))) - (((AffineMap (1 / 2),0 ) . 0 ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by C, FUNCT_1:23
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . ((2 * PI ) + 0 )))) - (((AffineMap (1 / 2),0 ) . 0 ) - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by JORDAN16:def 3
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . ((2 * PI ) + 0 )))) - (0 - (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )) by JORDAN16:25
.= ((((1 / 2) * PI ) - ((1 / 4) * (sin . ((2 * PI ) + 0 )))) - 0 ) + (((1 / 4) (#) (sin * (AffineMap 2,0 ))) . 0 )
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . ((2 * PI ) + 0 )))) + ((1 / 4) * ((sin * (AffineMap 2,0 )) . 0 )) by VALUED_1:6
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . ((2 * PI ) + 0 )))) + ((1 / 4) * (sin . ((AffineMap 2,0 ) . 0 ))) by C, FUNCT_1:23
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . (0 + ((2 * PI ) * 1))))) + ((1 / 4) * (sin . 0 )) by JORDAN16:25
.= (((1 / 2) * PI ) - ((1 / 4) * (sin . 0 ))) + ((1 / 4) * (sin . 0 )) by SIN_COS6:8
.= PI / 2 ;
hence integral (sin ^2 ),A = PI / 2 ; :: thesis: verum