let m, n be Element of NAT ; :: thesis: ( m + n <> 0 & m - n <> 0 implies ( ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) is_differentiable_on REAL & ( for x being 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)) ) ) )
assume that
A1: m + n <> 0 and
A2: m - n <> 0 ; :: thesis: ( ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) is_differentiable_on REAL & ( for x being 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)) ) )
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 FUNCT_2:def 1, JORDAN16:def 3;
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:28;
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: ( x in REAL implies (((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) `| REAL ) . x = (1 / 2) * (cos ((m - n) * x)) )
assume x in REAL ; :: thesis: (((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) `| REAL ) . x = (1 / 2) * (cos ((m - n) * x))
(((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:28
.= (1 / (2 * (m - n))) * (((sin * (AffineMap (m - n),0 )) `| REAL ) . x) by A4, FDIFF_1:def 8
.= (1 / (2 * (m - n))) * ((m - n) * (cos . (((m - n) * x) + 0 ))) by A3, FDIFF_4:37
.= ((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:75
.= (1 / 2) * (cos ((m - n) * x)) by A2, XCMPLX_1:92 ;
hence (((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) `| REAL ) . x = (1 / 2) * (cos ((m - n) * x)) ; :: thesis: verum

end;

A8: 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;
A9: ( 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 FUNCT_2:def 1, JORDAN16:def 3;
then A10: sin * (AffineMap (m + n),0 ) is_differentiable_on REAL by FDIFF_4:37;
A11: [#] REAL = dom ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) by FUNCT_2:def 1;
then A12: (1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 )) is_differentiable_on REAL by A10, FDIFF_1:28;
A13: 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: ( x in REAL implies (((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) `| REAL ) . x = (1 / 2) * (cos ((m + n) * x)) )
assume x in REAL ; :: thesis: (((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) `| REAL ) . x = (1 / 2) * (cos ((m + n) * x))
(((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) `| REAL ) . x = (1 / (2 * (m + n))) * (diff (sin * (AffineMap (m + n),0 )),x) by A11, A10, FDIFF_1:28
.= (1 / (2 * (m + n))) * (((sin * (AffineMap (m + n),0 )) `| REAL ) . x) by A10, FDIFF_1:def 8
.= (1 / (2 * (m + n))) * ((m + n) * (cos . (((m + n) * x) + 0 ))) by A9, FDIFF_4:37
.= ((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:75
.= (1 / 2) * (cos ((m + n) * x)) by A1, XCMPLX_1:92 ;
hence (((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) `| REAL ) . x = (1 / 2) * (cos ((m + n) * x)) ; :: thesis: verum

end;

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: ( x in REAL implies ((((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)) )
assume x in 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))
((((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 A8, A12, A6, FDIFF_1:26
.= ((((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) `| REAL ) . x) + (diff ((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))),x) by A12, FDIFF_1:def 8
.= ((((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 8
.= ((1 / 2) * (cos ((m + n) * x))) + ((((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) `| REAL ) . x) by A13
.= ((1 / 2) * (cos ((m + n) * x))) + ((1 / 2) * (cos ((m - n) * x))) by A7
.= (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:21
.= (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: verum

end;

hence ( ((1 / (2 * (m + n))) (#) (sin * (AffineMap (m + n),0 ))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap (m - n),0 ))) is_differentiable_on REAL & ( for x being 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)) ) ) by A8, A12, A6, FDIFF_1:26; :: thesis: verum