let m, n be Element of NAT ; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
assume A1: ( m + n <> 0 & m - n <> 0 ) ; :: thesis:
A2: for x being Real st x in REAL holds
(AffineMap (n,0)) . x = n * x

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
(AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def 4
.= n * x ;
hence (AffineMap (n,0)) . x = n * x ; :: thesis:

end;

A3: dom (cos * (AffineMap (n,0))) = [#] REAL by FUNCT_2:def 1;
A4: dom (cos * (AffineMap (m,0))) = [#] REAL by FUNCT_2:def 1;
then A5: (dom (cos * (AffineMap (m,0)))) /\ (dom (cos * (AffineMap (n,0)))) = [#] REAL by A3;
A6: for x being Real st x in REAL holds
(AffineMap (m,0)) . x = m * x

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
(AffineMap (m,0)) . x = (m * x) + 0 by FCONT_1:def 4
.= m * x ;
hence (AffineMap (m,0)) . x = m * x ; :: thesis:

end;

A7: 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 = ((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))) . x

let x be Real; :: thesis:
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 = (cos . (m * x)) * (cos . (n * x)) by A1, Th5
.= (cos . ((AffineMap (m,0)) . x)) * (cos . (n * x)) by A6
.= (cos . ((AffineMap (m,0)) . x)) * (cos . ((AffineMap (n,0)) . x)) by A2
.= ((cos * (AffineMap (m,0))) . x) * (cos . ((AffineMap (n,0)) . x)) by A4, FUNCT_1:12
.= ((cos * (AffineMap (m,0))) . x) * ((cos * (AffineMap (n,0))) . x) by A3, FUNCT_1:12
.= ((cos * (AffineMap (m,0))) (#) (cos * (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 = ((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))) . x ; :: thesis:

end;

A8: [#] REAL = dom ((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))) by FUNCT_2:def 1;
((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) is_differentiable_on REAL by A1, Th5;
then dom ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) `| REAL) = dom ((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))) by A8, FDIFF_1:def 7;
then A9: (((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) `| REAL = (cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0))) by A7, PARTFUN1:5;
A10: dom (AffineMap (n,0)) = [#] REAL by FUNCT_2:def 1;
( dom (AffineMap (m,0)) = REAL & ( for x being Real st x in REAL holds
(AffineMap (m,0)) . x = (m * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then (AffineMap (m,0)) | REAL is continuous by A10, FDIFF_1:23, FDIFF_1:25;
then A11: (AffineMap (m,0)) | A is continuous by FCONT_1:16;
cos | ((AffineMap (m,0)) .: A) is continuous ;
then A12: (cos * (AffineMap (m,0))) | A is continuous by A11, FCONT_1:25;
for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def 4;
then (AffineMap (n,0)) | REAL is continuous by A10, FDIFF_1:23, FDIFF_1:25;
then A13: (AffineMap (n,0)) | A is continuous by FCONT_1:16;
cos | ((AffineMap (n,0)) .: A) is continuous ;
then A14: (cos * (AffineMap (n,0))) | A is continuous by A13, FCONT_1:25;
then ((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))) | A is continuous by A5, A12, FCONT_1:18;
then A15: (cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0))) is_integrable_on A by A8, INTEGRA5:11;
((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))) | A is bounded by A8, A5, A14, A12, FCONT_1:18, INTEGRA5:10;
hence integral (((cos * (AffineMap (m,0))) (#) (cos * (AffineMap (n,0)))),A) = ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) . (upper_bound A)) - ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) . (lower_bound A)) by A1, A15, A9, Th5, INTEGRA5:13; :: thesis: