let m, n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
integral ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))),A = ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (sup A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (inf A))
let A be closed-interval Subset of REAL ; :: thesis: ( m + n <> 0 & m - n <> 0 implies integral ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))),A = ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (sup A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (inf A)) )
assume A1: ( m + n <> 0 & m - n <> 0 ) ; :: thesis: integral ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))),A = ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (sup A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (inf A))
( dom (AffineMap n,0 ) = [#] REAL & ( 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;
( dom (AffineMap m,0 ) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap m,0 ) . x = (m * x) + 0 ) ) by FUNCT_2:def 1, JORDAN16:def 3;
then (AffineMap m,0 ) | REAL is continuous by FDIFF_1:31, FDIFF_1:33;
then A3: (AffineMap m,0 ) | A is continuous by FCONT_1:17;
sin | ((AffineMap m,0 ) .: A) is continuous ;
then A4: (sin * (AffineMap m,0 )) | A is continuous by A3, FCONT_1:26;
A5: 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: dom (sin * (AffineMap n,0 )) = [#] REAL by FUNCT_2:def 1;
A7: dom (sin * (AffineMap m,0 )) = [#] REAL by FUNCT_2:def 1;
then A8: (dom (sin * (AffineMap m,0 ))) /\ (dom (sin * (AffineMap n,0 ))) = [#] REAL by A6;
A9: for x being Real st x in REAL holds
(AffineMap m,0 ) . x = m * x

proof

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

end;

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

proof

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

end;

A11: REAL = dom ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))) by FUNCT_2:def 1;
sin | ((AffineMap n,0 ) .: A) is continuous ;
then A12: (sin * (AffineMap n,0 )) | A is continuous by A2, FCONT_1:26;
then ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))) | A is continuous by A8, A4, FCONT_1:19;
then A13: (sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 )) is_integrable_on A by A11, INTEGRA5:11;
((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) is_differentiable_on REAL by A1, Th6;
then dom ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) `| REAL ) = dom ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))) by A11, FDIFF_1:def 8;
then A14: (((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) `| REAL = (sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 )) by A10, PARTFUN1:34;
((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))) | A is bounded by A11, A8, A12, A4, FCONT_1:19, INTEGRA5:10;
hence integral ((sin * (AffineMap m,0 )) (#) (sin * (AffineMap n,0 ))),A = ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (sup A)) - ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )))) . (inf A)) by A1, A13, A14, Th6, INTEGRA5:13; :: thesis: verum