let A be non empty closed_interval Subset of REAL; :: thesis: integral ((sin ^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 = (sin ^2) . x

proof

let x be Element of 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 = (sin ^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 = (sin ^2) . x
(((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (sin . x) ^2 by Th1
.= (sin ^2) . x by VALUED_1:11 ;
hence (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (sin ^2) . x ; :: thesis: verum

end;

A2: dom (sin ^2) = REAL by SIN_COS:24, VALUED_1:11;
then dom (((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) = dom (sin ^2) by Th1, FDIFF_1:def 7;
then A3: ((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL = sin ^2 by A1, PARTFUN1:5;
(sin ^2) | A is bounded by A2, INTEGRA5:10;
hence integral ((sin ^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, Th1, INTEGRA5:11, INTEGRA5:13; :: thesis: verum