let n be Element of NAT ; :: thesis: ( n <> 0 implies ( ((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)) ) ) )
A1: dom (((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (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 FUNCT_2:def 1, JORDAN16:def 3;
then A3: AffineMap (1 / n),0 is_differentiable_on REAL by A1, FDIFF_1:31;
A4: for x being Real st x in REAL holds
(AffineMap n,0 ) . x = (n * x) + 0 by JORDAN16:def 3;
A5: dom (sin * (AffineMap n,0 )) = [#] REAL by FUNCT_2:def 1;
then A6: sin * (AffineMap n,0 ) is_differentiable_on REAL by A4, FDIFF_4:37;
A7: dom ((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) = REAL by FUNCT_2:def 1;
then A8: (1 / (n ^2 )) (#) (sin * (AffineMap n,0 )) is_differentiable_on REAL by A1, A6, FDIFF_1:28;
assume A9: n <> 0 ; :: thesis: ( ((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)) ) )
A10: 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: ( x in REAL implies (((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = (1 / n) * (cos (n * x)) )
assume x in REAL ; :: thesis: (((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = (1 / n) * (cos (n * x))
(((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = (1 / (n ^2 )) * (diff (sin * (AffineMap n,0 )),x) by A7, A1, A6, FDIFF_1:28
.= (1 / (n ^2 )) * (((sin * (AffineMap n,0 )) `| REAL ) . x) by A6, FDIFF_1:def 8
.= (1 / (n ^2 )) * (n * (cos . ((n * x) + 0 ))) by A5, A4, 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 A9, XCMPLX_1:92 ;
hence (((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = (1 / n) * (cos (n * x)) ; :: thesis: verum

end;

A11: dom (cos * (AffineMap n,0 )) = [#] REAL by FUNCT_2:def 1;
then A12: cos * (AffineMap n,0 ) is_differentiable_on REAL by A4, FDIFF_4:38;
A13: dom ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))) = REAL by FUNCT_2:def 1;
then A14: (AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )) is_differentiable_on REAL by A1, A3, A12, FDIFF_1:29;
A15: 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: ( x in REAL implies (((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (cos . (n * x))) - (x * (sin . (n * x))) )
assume x in REAL ; :: thesis: (((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (cos . (n * x))) - (x * (sin . (n * x)))
(((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 A13, A1, A3, A12, 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 A3, FDIFF_1:def 8
.= (((cos * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (diff (cos * (AffineMap n,0 )),x)) by A1, A2, FDIFF_1:31
.= (((cos * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (((cos * (AffineMap n,0 )) `| REAL ) . x)) by A12, FDIFF_1:def 8
.= (((cos * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (- (n * (sin . ((n * x) + 0 ))))) by A11, A4, 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 A11, 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 A9, 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: verum

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: ( x in REAL implies ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) `| REAL ) . x = x * (sin . (n * x)) )
assume x in REAL ; :: thesis: ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) - ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 )))) `| REAL ) . x = x * (sin . (n * x))
((((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, A8, A14, FDIFF_1:27
.= ((((1 / (n ^2 )) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x) - (diff ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))),x) by A8, FDIFF_1:def 8
.= ((1 / n) * (cos (n * x))) - (diff ((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))),x) by A10
.= ((1 / n) * (cos (n * x))) - ((((AffineMap (1 / n),0 ) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x) by A14, FDIFF_1:def 8
.= ((1 / n) * (cos (n * x))) - (((1 / n) * (cos . (n * x))) - (x * (sin . (n * x)))) by A15
.= 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: verum

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, A8, A14, FDIFF_1:27; :: thesis: verum