let A be non empty closed_interval Subset of REAL; integral ((cos ^2),A) = (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (upper_bound A)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (lower_bound A))
A1:
for x being Element of REAL st x in dom (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) holds
(((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos ^2) . x
proof
let x be
Element of
REAL ;
( x in dom (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) implies (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos ^2) . x )
assume
x in dom (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL)
;
(((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos ^2) . x
(((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x =
(cos . x) ^2
by Th2
.=
(cos ^2) . x
by VALUED_1:11
;
hence
(((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos ^2) . x
;
verum
end;
A2:
dom (cos ^2) = REAL
by SIN_COS:24, VALUED_1:11;
then
dom (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) = dom (cos ^2)
by Th2, FDIFF_1:def 7;
then A3:
((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL = cos ^2
by A1, PARTFUN1:5;
(cos ^2) | A is bounded
by A2, INTEGRA5:10;
hence
integral ((cos ^2),A) = (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (upper_bound A)) - (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) . (lower_bound A))
by A2, A3, Th2, INTEGRA5:11, INTEGRA5:13; verum