let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL st n <> 0 holds
integral (((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (upper_bound A)) - ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (lower_bound A))
let A be closed-interval Subset of REAL; :: thesis: ( n <> 0 implies integral (((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (upper_bound A)) - ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (lower_bound A)) )
assume A1: n <> 0 ; :: thesis: integral (((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (upper_bound A)) - ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (lower_bound A))
( [#] REAL = dom (AffineMap (n,0)) & ( for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0 ) ) by FUNCT_2:def 1, JORDAN16:def 3;
then (AffineMap (n,0)) | REAL is continuous by FDIFF_1:31, FDIFF_1:33;
then A2: (AffineMap (n,0)) | A is continuous by FCONT_1:17;
sin | ((AffineMap (n,0)) .: A) is continuous ;
then A3: (sin * (AffineMap (n,0))) | A is continuous by A2, FCONT_1:26;
A4: for x being Real st x in REAL holds
(AffineMap (n,0)) . x = n * x

proof

let x be Real; :: thesis: ( x in REAL implies (AffineMap (n,0)) . x = n * x )
assume x in REAL ; :: thesis: (AffineMap (n,0)) . x = n * x
(AffineMap (n,0)) . x = (n * x) + 0 by JORDAN16:def 3
.= n * x ;
hence (AffineMap (n,0)) . x = n * x ; :: thesis: verum

end;

A5: dom (sin * (AffineMap (n,0))) = [#] REAL by FUNCT_2:def 1;
A6: for x being Real st x in REAL holds
(AffineMap (1,0)) . x = x

proof

let x be Real; :: thesis: ( x in REAL implies (AffineMap (1,0)) . x = x )
assume x in REAL ; :: thesis: (AffineMap (1,0)) . x = x
(AffineMap (1,0)) . x = (1 * x) + 0 by JORDAN16:def 3
.= x ;
hence (AffineMap (1,0)) . x = x ; :: thesis: verum

end;

A7: for x being Real st x in dom ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) holds
((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) . x

proof

let x be Real; :: thesis: ( x in dom ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) implies ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) . x )
assume x in dom ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) ; :: thesis: ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) . x
((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = x * (sin . (n * x)) by A1, Th8
.= x * (sin . ((AffineMap (n,0)) . x)) by A4
.= x * ((sin * (AffineMap (n,0))) . x) by A5, FUNCT_1:22
.= ((AffineMap (1,0)) . x) * ((sin * (AffineMap (n,0))) . x) by A6
.= ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) . x by VALUED_1:5 ;
hence ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) . x ; :: thesis: verum

end;

A8: dom ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) = [#] REAL by FUNCT_2:def 1;
((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0)))) is_differentiable_on REAL by A1, Th8;
then dom ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) = dom ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) by A8, FDIFF_1:def 8;
then A9: (((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL = (AffineMap (1,0)) (#) (sin * (AffineMap (n,0))) by A7, PARTFUN1:34;
A10: dom (AffineMap (1,0)) = [#] REAL by FUNCT_2:def 1;
then A11: (dom (AffineMap (1,0))) /\ (dom (sin * (AffineMap (n,0)))) = [#] REAL by A5;
for x being Real st x in REAL holds
(AffineMap (1,0)) . x = (1 * x) + 0 by JORDAN16:def 3;
then (AffineMap (1,0)) | REAL is continuous by A10, FDIFF_1:31, FDIFF_1:33;
then A12: (AffineMap (1,0)) | A is continuous by FCONT_1:17;
then ((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) | A is continuous by A11, A3, FCONT_1:19;
then A13: (AffineMap (1,0)) (#) (sin * (AffineMap (n,0))) is_integrable_on A by A8, INTEGRA5:11;
((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))) | A is bounded by A8, A11, A3, A12, FCONT_1:19, INTEGRA5:10;
hence integral (((AffineMap (1,0)) (#) (sin * (AffineMap (n,0)))),A) = ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (upper_bound A)) - ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) . (lower_bound A)) by A1, A13, A9, Th8, INTEGRA5:13; :: thesis: verum