let A be closed-interval Subset of REAL ; :: thesis: 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 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 Real; :: thesis: ( 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 ) ; :: thesis: (((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 ; :: thesis: verum

end;

A2: dom (cos ^2 ) = REAL by SIN_COS:27, VALUED_1:11;
then dom (((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) = dom (cos ^2 ) by Th2, FDIFF_1:def 8;
then A3: ((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL = cos ^2 by A1, PARTFUN1:34;
(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; :: thesis: verum