let n, m be Element of NAT ; :: thesis:
assume that
A1: m + n <> 0 and
A2: m - n <> 0 ; :: thesis:
A3: ( dom (sin * (AffineMap ((m - n),0))) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap ((m - n),0)) . x = ((m - n) * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then A4: sin * (AffineMap ((m - n),0)) is_differentiable_on REAL by FDIFF_4:37;
A5: dom ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) = [#] REAL by FUNCT_2:def 1;
then A6: (1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))) is_differentiable_on REAL by A4, FDIFF_1:20;
A7: for x being Real st x in REAL holds
(((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) `| REAL) . x = (1 / 2) * (cos ((m - n) * x))

proof

let x be Real; :: thesis:
assume A8: x in REAL ; :: thesis:
(((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) `| REAL) . x = (1 / (2 * (m - n))) * (diff ((sin * (AffineMap ((m - n),0))),x)) by A5, A4, FDIFF_1:20, A8
.= (1 / (2 * (m - n))) * (((sin * (AffineMap ((m - n),0))) `| REAL) . x) by A4, FDIFF_1:def 7, A8
.= (1 / (2 * (m - n))) * ((m - n) * (cos . (((m - n) * x) + 0))) by A3, FDIFF_4:37, A8
.= ((m - n) * (1 / (2 * (m - n)))) * (cos . (((m - n) * x) + 0))
.= ((1 * (m - n)) / (2 * (m - n))) * (cos . (((m - n) * x) + 0)) by XCMPLX_1:74
.= (1 / 2) * (cos ((m - n) * x)) by A2, XCMPLX_1:91 ;
hence (((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) `| REAL) . x = (1 / 2) * (cos ((m - n) * x)) ; :: thesis:

end;

A9: dom (((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) = [#] REAL by FUNCT_2:def 1;
A10: ( dom (sin * (AffineMap ((m + n),0))) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap ((m + n),0)) . x = ((m + n) * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then A11: sin * (AffineMap ((m + n),0)) is_differentiable_on REAL by FDIFF_4:37;
A12: [#] REAL = dom ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) by FUNCT_2:def 1;
then A13: (1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0))) is_differentiable_on REAL by A11, FDIFF_1:20;
hence ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) is_differentiable_on REAL by A9, A6, FDIFF_1:18; :: thesis:
A14: for x being Real st x in REAL holds
(((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) `| REAL) . x = (1 / 2) * (cos ((m + n) * x))

proof

let x be Real; :: thesis:
assume A15: x in REAL ; :: thesis:
(((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) `| REAL) . x = (1 / (2 * (m + n))) * (diff ((sin * (AffineMap ((m + n),0))),x)) by A12, A11, FDIFF_1:20, A15
.= (1 / (2 * (m + n))) * (((sin * (AffineMap ((m + n),0))) `| REAL) . x) by A11, FDIFF_1:def 7, A15
.= (1 / (2 * (m + n))) * ((m + n) * (cos . (((m + n) * x) + 0))) by A10, FDIFF_4:37, A15
.= ((m + n) * (1 / (2 * (m + n)))) * (cos . (((m + n) * x) + 0))
.= ((1 * (m + n)) / (2 * (m + n))) * (cos . (((m + n) * x) + 0)) by XCMPLX_1:74
.= (1 / 2) * (cos ((m + n) * x)) by A1, XCMPLX_1:91 ;
hence (((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) `| REAL) . x = (1 / 2) * (cos ((m + n) * x)) ; :: thesis:

end;

A16: for x being Real st x in REAL holds
((((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))

proof

let x be Real; :: thesis:
assume A17: x in REAL ; :: thesis:
((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) `| REAL) . x = (diff (((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))),x)) + (diff (((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))),x)) by A9, A13, A6, FDIFF_1:18, A17
.= ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) `| REAL) . x) + (diff (((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))),x)) by A13, FDIFF_1:def 7, A17
.= ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) `| REAL) . x) + ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) `| REAL) . x) by A6, FDIFF_1:def 7, A17
.= ((1 / 2) * (cos ((m + n) * x))) + ((((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) `| REAL) . x) by A14, A17
.= ((1 / 2) * (cos ((m + n) * x))) + ((1 / 2) * (cos ((m - n) * x))) by A7, A17
.= (1 / 2) * ((cos ((m + n) * x)) + (cos ((m - n) * x)))
.= (1 / 2) * (2 * ((cos ((((m + n) * x) + ((m - n) * x)) / 2)) * (cos ((((m + n) * x) - ((m - n) * x)) / 2)))) by SIN_COS4:17
.= (cos . (m * x)) * (cos . (n * x)) ;
hence ((((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)) ; :: thesis:

end;

let x be Real; :: thesis:
x in REAL by XREAL_0:def 1;
hence ((((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 A16; :: thesis: