let A be non empty closed_interval Subset of REAL; ( A = [.0,(2 * PI).] implies integral ((sin ^2),A) = PI )
assume
A = [.0,(2 * PI).]
; 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))))) . dp) - (((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, Lm6
.=
((((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 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)))) - 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, Lm6, FUNCT_1:13
.=
(((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 ((sin ^2),A) = PI
; verum