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

proof

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
(((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = (1 / (n ^2 )) * (diff (cos * (AffineMap n,0 )),x) by A1, A3, FDIFF_1:28
.= (1 / (n ^2 )) * (((cos * (AffineMap n,0 )) `| REAL ) . x) by A3, FDIFF_1:def 8
.= (1 / (n ^2 )) * (- (n * (sin . ((n * x) + 0 )))) by A1, A2, FDIFF_4:38
.= ((- 1) * (n * (1 / (n * n)))) * (sin . ((n * x) + 0 ))
.= ((- 1) * (n / ((n * n) / 1))) * (sin . ((n * x) + 0 )) by XCMPLX_1:80
.= ((- 1) * ((n * 1) / (n * n))) * (sin . ((n * x) + 0 ))
.= ((- 1) * (1 / n)) * (sin . ((n * x) + 0 )) by A, XCMPLX_1:92 ;
hence (((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = - ((1 / n) * (sin (n * x))) ; :: thesis:

end;

B1: for x being Real st x in REAL holds
(AffineMap (1 / n),0 ) . x = ((1 / n) * x) + 0 by JORDAN16:def 3;
then A6: ( AffineMap (1 / n),0 is_differentiable_on REAL & ( for x being Real st x in REAL holds
((AffineMap (1 / n),0 ) `| REAL ) . x = 1 / n ) ) by A1, FDIFF_1:31;
A7: ( sin * (AffineMap n,0 ) is_differentiable_on REAL & ( for x being Real st x in REAL holds
((sin * (AffineMap n,0 )) `| REAL ) . x = n * (cos . ((n * x) + 0 )) ) ) by A1, A2, FDIFF_4:37;
then A8: (AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 )) is_differentiable_on REAL by A1, A6, FDIFF_1:29;
A9: for x being Real st x in REAL holds
(((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))

proof

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
(((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = (((sin * (AffineMap n,0 )) . x) * (diff (AffineMap (1 / n),0 ),x)) + (((AffineMap (1 / n),0 ) . x) * (diff (sin * (AffineMap n,0 )),x)) by A1, A6, A7, FDIFF_1:29
.= (((sin * (AffineMap n,0 )) . x) * (((AffineMap (1 / n),0 ) `| REAL ) . x)) + (((AffineMap (1 / n),0 ) . x) * (diff (sin * (AffineMap n,0 )),x)) by A6, FDIFF_1:def 8
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (diff (sin * (AffineMap n,0 )),x)) by A1, B1, FDIFF_1:31
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (((sin * (AffineMap n,0 )) `| REAL ) . x)) by A7, FDIFF_1:def 8
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (n * (cos . ((n * x) + 0 )))) by A1, A2, FDIFF_4:37
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + ((((1 / n) * x) + 0 ) * (n * (cos . ((n * x) + 0 )))) by JORDAN16:def 3
.= ((sin . ((AffineMap n,0 ) . x)) * (1 / n)) + (((1 / n) * x) * (n * (cos . ((n * x) + 0 )))) by A1, FUNCT_1:22
.= ((1 / n) * (sin . (n * x))) + ((((1 / n) * n) * x) * (cos . (n * x))) by JORDAN16:def 3
.= ((1 / n) * (sin . (n * x))) + ((1 * x) * (cos . (n * x))) by A, XCMPLX_1:88
.= ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x))) ;
hence (((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x))) ; :: thesis:

end;

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

proof

let x be Real; :: thesis:
assume x in REAL ; :: thesis:
((((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) + ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 )))) `| REAL ) . x = (diff ((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))),x) + (diff ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))),x) by A1, A4, A8, FDIFF_1:26
.= ((((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x) + (diff ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))),x) by A4, FDIFF_1:def 8
.= (- ((1 / n) * (sin (n * x)))) + (diff ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))),x) by A5
.= (- ((1 / n) * (sin (n * x)))) + ((((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x) by A8, FDIFF_1:def 8
.= (- ((1 / n) * (sin (n * x)))) + (((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))) by A9
.= x * (cos . (n * x)) ;
hence ((((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) + ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 )))) `| REAL ) . x = x * (cos . (n * x)) ; :: thesis:

end;

hence ( ((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) + ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) + ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 )))) `| REAL ) . x = x * (cos . (n * x)) ) ) by A1, A4, A8, FDIFF_1:26; :: thesis: