let n be Element of NAT ; :: thesis:
assume A: n <> 0 ; :: thesis:
A1: ( dom ((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) = REAL & dom ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))) = REAL & dom (((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (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: ( 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, FDIFF_4:37;
then A4: (1 / (n ^2 )) (#) (sin * (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 )) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = (1 / n) * (cos (n * x))

proof

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

proof

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

end;

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

proof

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

end;

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