let A be non empty 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 ( upper_bound A = PI & lower_bound A = 0 ) by INTEGRA8:37;
then integral ((sin ^2),A) = (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) . pp) - (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) . 0) by 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 Lm5, 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 Lm5, VALUED_1:13, Lm6
.= ((((1 / 2) * PI) + 0) - (((1 / 4) (#) (sin * (AffineMap (2,0)))) . PI)) - (((AffineMap ((1 / 2),0)) . 0) - (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by FCONT_1:def 4
.= (((1 / 2) * PI) - ((1 / 4) * ((sin * (AffineMap (2,0))) . pp))) - (((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 Lm4, FUNCT_1:13
.= (((1 / 2) * PI) - ((1 / 4) * (sin . ((2 * PI) + 0)))) - (((AffineMap ((1 / 2),0)) . 0) - (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by FCONT_1:def 4
.= (((1 / 2) * PI) - ((1 / 4) * (sin . ((2 * PI) + 0)))) - (0 - (((1 / 4) (#) (sin * (AffineMap (2,0)))) . 0)) by FCONT_1:48
.= ((((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 Lm4, FUNCT_1:13, Lm6
.= (((1 / 2) * PI) - ((1 / 4) * (sin . (0 + ((2 * PI) * 1))))) + ((1 / 4) * (sin . 0)) by FCONT_1:48
.= (((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