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 )))) . (sup A)) - ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) . (inf 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 )))) . (sup A)) - ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) . (inf A)) )
assume A: 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 )))) . (sup A)) - ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) . (inf A))
A1: ( dom ((AffineMap 1,0 ) (#) (sin * (AffineMap n,0 ))) = [#] REAL & dom (AffineMap 1,0 ) = [#] REAL & dom (sin * (AffineMap n,0 )) = [#] REAL & [#] REAL = dom (AffineMap n,0 ) ) by FUNCT_2:def 1;
then C: (dom (AffineMap 1,0 )) /\ (dom (sin * (AffineMap n,0 ))) = [#] REAL ;
for x being Real st x in REAL holds
(AffineMap n,0 ) . x = (n * x) + 0 by JORDAN16:def 3;
then (AffineMap n,0 ) | REAL is continuous by A1, 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;
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 A1, FDIFF_1:31, FDIFF_1:33;
then A4: (AffineMap 1,0 ) | A is continuous by FCONT_1:17;
((AffineMap 1,0 ) (#) (sin * (AffineMap n,0 ))) | A is continuous by C, A3, A4, FCONT_1:19;
then A5: ( (AffineMap 1,0 ) (#) (sin * (AffineMap n,0 )) is_integrable_on A & ((AffineMap 1,0 ) (#) (sin * (AffineMap n,0 ))) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
B1: 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;

B2: 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;

A6: ((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))) is_differentiable_on REAL by A, Th8;
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 A, Th8
.= x * (sin . ((AffineMap n,0 ) . x)) by B2
.= x * ((sin * (AffineMap n,0 )) . x) by A1, FUNCT_1:22
.= ((AffineMap 1,0 ) . x) * ((sin * (AffineMap n,0 )) . x) by B1
.= ((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;

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 A1, A6, FDIFF_1:def 8;
then (((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;
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 )))) . (sup A)) - ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) . (inf A)) by A, A5, Th8, INTEGRA5:13; :: thesis: verum