let A be non empty closed_interval Subset of REAL; ( A = [.0,PI.] implies integral ((cos ^2),A) = PI / 2 )
assume
A = [.0,PI.]
; integral ((cos ^2),A) = PI / 2
then
( upper_bound A = PI & lower_bound A = 0 )
by INTEGRA8:37;
then integral ((cos ^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 Th16
.=
(((AffineMap ((1 / 2),0)) . PI) + (((1 / 4) (#) (sin * (AffineMap (2,0)))) . pp)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . 0)
by VALUED_1:1
.=
(((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 VALUED_1:1, 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))) . 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)) . pp)))) - (((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)))) - ((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 ((cos ^2),A) = PI / 2
; verum