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

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
A6: dom (((- 1) / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 ))) = [#] REAL by FUNCT_2:def 1;
((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) `| REAL ) . x = ((((- 1) * (1 / (2 * (m + n)))) (#) (cos * (AffineMap (m + n),0 ))) `| REAL ) . x by RFUNCT_1:29
.= (((- (1 / (2 * (m + n)))) (#) (cos * (AffineMap (m + n),0 ))) `| REAL ) . x
.= ((((- 1) / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 ))) `| REAL ) . x by XCMPLX_1:188
.= ((- 1) / (2 * (m + n))) * (diff (cos * (AffineMap (m + n),0 )),x) by A4, A6, FDIFF_1:28
.= ((- 1) / (2 * (m + n))) * (((cos * (AffineMap (m + n),0 )) `| REAL ) . x) by A4, FDIFF_1:def 8
.= ((- 1) / (2 * (m + n))) * (- ((m + n) * (sin . (((m + n) * x) + 0 )))) by A3, FDIFF_4:38
.= ((- ((- 1) / (2 * (m + n)))) * (m + n)) * (sin . (((m + n) * x) + 0 ))
.= ((1 / (2 * (m + n))) * (m + n)) * (sin . (((m + n) * x) + 0 )) by XCMPLX_1:191
.= ((1 * (m + n)) / (2 * (m + n))) * (sin . (((m + n) * x) + 0 )) by XCMPLX_1:75
.= (1 / 2) * (sin ((m + n) * x)) by A1, XCMPLX_1:92 ;
hence ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) `| REAL ) . x = (1 / 2) * (sin ((m + n) * x)) ; :: thesis:

end;

A7: dom (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) = [#] REAL by FUNCT_2:def 1;
dom ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 ))) = [#] REAL by FUNCT_2:def 1;
then ( - ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 ))) = (- 1) (#) ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 ))) & (1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )) is_differentiable_on REAL ) by A4, FDIFF_1:28;
then A8: - ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 ))) is_differentiable_on REAL by A7, FDIFF_1:28;
A9: REAL = dom ((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 )))) by FUNCT_2:def 1;
A10: ( dom (cos * (AffineMap (m - n),0 )) = [#] REAL & ( for x being Real st x in REAL holds
(AffineMap (m - n),0 ) . x = ((m - n) * x) + 0 ) ) by FUNCT_2:def 1, JORDAN16:def 3;
then A11: cos * (AffineMap (m - n),0 ) is_differentiable_on REAL by FDIFF_4:38;
A12: dom ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) = [#] REAL by FUNCT_2:def 1;
then A13: (1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 )) is_differentiable_on REAL by A11, FDIFF_1:28;
A14: for x being Real st x in REAL holds
(((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) `| REAL ) . x = - ((1 / 2) * (sin ((m - n) * x)))

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
(((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) `| REAL ) . x = (1 / (2 * (m - n))) * (diff (cos * (AffineMap (m - n),0 )),x) by A12, A11, FDIFF_1:28
.= (1 / (2 * (m - n))) * (((cos * (AffineMap (m - n),0 )) `| REAL ) . x) by A11, FDIFF_1:def 8
.= (1 / (2 * (m - n))) * (- ((m - n) * (sin . (((m - n) * x) + 0 )))) by A10, FDIFF_4:38
.= ((- (1 / (2 * (m - n)))) * (m - n)) * (sin . (((m - n) * x) + 0 ))
.= (((- 1) / (2 * (m - n))) * (m - n)) * (sin . (((m - n) * x) + 0 )) by XCMPLX_1:188
.= (((- 1) * (m - n)) / (2 * (m - n))) * (sin . (((m - n) * x) + 0 )) by XCMPLX_1:75
.= ((- 1) / 2) * (sin ((m - n) * x)) by A2, XCMPLX_1:92 ;
hence (((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) `| REAL ) . x = - ((1 / 2) * (sin ((m - n) * x))) ; :: thesis:

end;

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

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
(((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 )))) `| REAL ) . x = (diff (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))),x) - (diff ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))),x) by A7, A9, A8, A13, FDIFF_1:27
.= (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) `| REAL ) . x) - (diff ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))),x) by A8, FDIFF_1:def 8
.= (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) `| REAL ) . x) - ((((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) `| REAL ) . x) by A13, FDIFF_1:def 8
.= ((1 / 2) * (sin ((m + n) * x))) - ((((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) `| REAL ) . x) by A5
.= ((1 / 2) * (sin ((m + n) * x))) - (- ((1 / 2) * (sin ((m - n) * x)))) by A14
.= (1 / 2) * ((sin ((m + n) * x)) + (sin ((m - n) * x)))
.= (1 / 2) * (2 * ((cos ((((m + n) * x) - ((m - n) * x)) / 2)) * (sin ((((m + n) * x) + ((m - n) * x)) / 2)))) by SIN_COS4:19
.= (sin . (m * x)) * (cos . (n * x)) ;
hence (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 )))) `| REAL ) . x = (sin . (m * x)) * (cos . (n * x)) ; :: thesis:

end;

hence ( (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 ))) is_differentiable_on REAL & ( for x being Real holds (((- ((1 / (2 * (m + n))) (#) (cos * (AffineMap (m + n),0 )))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap (m - n),0 )))) `| REAL ) . x = (sin . (m * x)) * (cos . (n * x)) ) ) by A7, A9, A8, A13, FDIFF_1:27; :: thesis: