let A be closed-interval Subset of REAL ; :: thesis: integral (sin ^2 ),A = (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . (sup A)) - (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . (inf A))
A1: dom (sin ^2 ) = REAL by SIN_COS:27, VALUED_1:11;
(sin (#) sin ) | A is continuous ;
then A2: ( sin ^2 is_integrable_on A & (sin ^2 ) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A3: 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 = (sin ^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 = (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;

dom (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) = dom (sin ^2 ) by A1, Th1, FDIFF_1:def 8;
then ((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL = sin ^2 by A3, PARTFUN1:34;
hence integral (sin ^2 ),A = (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . (sup A)) - (((AffineMap (1 / 2),0 ) - ((1 / 4) (#) (sin * (AffineMap 2,0 )))) . (inf A)) by A2, Th1, INTEGRA5:13; :: thesis: verum