let n be Element of NAT ; :: thesis:
A1: dom (((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) = [#] REAL by FUNCT_2:def 1;
A2: ( dom (AffineMap ((1 / n),0)) = REAL & ( for x being Real st x in REAL holds
(AffineMap ((1 / n),0)) . x = ((1 / n) * x) + 0 ) ) by FCONT_1:def 4, FUNCT_2:def 1;
then A3: AffineMap ((1 / n),0) is_differentiable_on REAL by A1, FDIFF_1:23;
A4: for x being Real st x in REAL holds
(AffineMap (n,0)) . x = (n * x) + 0 by FCONT_1:def 4;
A5: dom (cos * (AffineMap (n,0))) = [#] REAL by FUNCT_2:def 1;
then A6: cos * (AffineMap (n,0)) is_differentiable_on REAL by A4, FDIFF_4:38;
A7: dom ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) = REAL by FUNCT_2:def 1;
then A8: (1 / (n ^2)) (#) (cos * (AffineMap (n,0))) is_differentiable_on REAL by A1, A6, FDIFF_1:20;
assume A9: n <> 0 ; :: thesis:
A10: 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 A11: x in REAL ; :: thesis:
(((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = (1 / (n ^2)) * (diff ((cos * (AffineMap (n,0))),x)) by A7, A1, A6, FDIFF_1:20, A11
.= (1 / (n ^2)) * (((cos * (AffineMap (n,0))) `| REAL) . x) by A6, FDIFF_1:def 7, A11
.= (1 / (n ^2)) * (- (n * (sin . ((n * x) + 0)))) by A5, A4, FDIFF_4:38, A11
.= ((- 1) * (n * (1 / (n * n)))) * (sin . ((n * x) + 0))
.= ((- 1) * (n / ((n * n) / 1))) * (sin . ((n * x) + 0)) by XCMPLX_1:79
.= ((- 1) * ((n * 1) / (n * n))) * (sin . ((n * x) + 0))
.= ((- 1) * (1 / n)) * (sin . ((n * x) + 0)) by A9, XCMPLX_1:91 ;
hence (((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x = - ((1 / n) * (sin (n * x))) ; :: thesis:

end;

A12: dom (sin * (AffineMap (n,0))) = [#] REAL by FUNCT_2:def 1;
then A13: sin * (AffineMap (n,0)) is_differentiable_on REAL by A4, FDIFF_4:37;
A14: dom ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) = REAL by FUNCT_2:def 1;
then A15: (AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL by A1, A3, A13, FDIFF_1:21;
hence ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) is_differentiable_on REAL by A1, A8, FDIFF_1:18; :: thesis:
A16: 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 A17: 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 A14, A1, A3, A13, FDIFF_1:21, A17
.= (((sin * (AffineMap (n,0))) . x) * (((AffineMap ((1 / n),0)) `| REAL) . x)) + (((AffineMap ((1 / n),0)) . x) * (diff ((sin * (AffineMap (n,0))),x))) by A3, FDIFF_1:def 7, A17
.= (((sin * (AffineMap (n,0))) . x) * (1 / n)) + (((AffineMap ((1 / n),0)) . x) * (diff ((sin * (AffineMap (n,0))),x))) by A1, A2, FDIFF_1:23, A17
.= (((sin * (AffineMap (n,0))) . x) * (1 / n)) + (((AffineMap ((1 / n),0)) . x) * (((sin * (AffineMap (n,0))) `| REAL) . x)) by A13, FDIFF_1:def 7, A17
.= (((sin * (AffineMap (n,0))) . x) * (1 / n)) + (((AffineMap ((1 / n),0)) . x) * (n * (cos . ((n * x) + 0)))) by A12, A4, FDIFF_4:37, A17
.= (((sin * (AffineMap (n,0))) . x) * (1 / n)) + ((((1 / n) * x) + 0) * (n * (cos . ((n * x) + 0)))) by FCONT_1:def 4
.= ((sin . ((AffineMap (n,0)) . x)) * (1 / n)) + (((1 / n) * x) * (n * (cos . ((n * x) + 0)))) by A12, FUNCT_1:12, A17
.= ((1 / n) * (sin . (n * x))) + ((((1 / n) * n) * x) * (cos . (n * x))) by FCONT_1:def 4
.= ((1 / n) * (sin . (n * x))) + ((1 * x) * (cos . (n * x))) by A9, XCMPLX_1:87
.= ((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;

A18: 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 A19: 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, A8, A15, FDIFF_1:18, A19
.= ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) `| REAL) . x) + (diff (((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))),x)) by A8, FDIFF_1:def 7, A19
.= (- ((1 / n) * (sin (n * x)))) + (diff (((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))),x)) by A10, A19
.= (- ((1 / n) * (sin (n * x)))) + ((((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) `| REAL) . x) by A15, FDIFF_1:def 7, A19
.= (- ((1 / n) * (sin (n * x)))) + (((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))) by A16, A19
.= 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;

let x be Real; :: thesis:
x in REAL by XREAL_0:def 1;
hence ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) by A18; :: thesis: