let n be Element of NAT ; :: thesis: ( n <> 0 implies ( ((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)) ) ) )
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 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 (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:28;
assume A9: n <> 0 ; :: thesis: ( ((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)) ) )
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: ( x in REAL implies (((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = - ((1 / n) * (sin (n * x))) )
assume x in REAL ; :: thesis: (((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = - ((1 / n) * (sin (n * x)))
(((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = (1 / (n ^2 )) * (diff (cos * (AffineMap n,0 )),x) by A7, A1, A6, FDIFF_1:28
.= (1 / (n ^2 )) * (((cos * (AffineMap n,0 )) `| REAL ) . x) by A6, FDIFF_1:def 8
.= (1 / (n ^2 )) * (- (n * (sin . ((n * x) + 0 )))) by A5, A4, 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 A9, XCMPLX_1:92 ;
hence (((1 / (n ^2 )) (#) (cos * (AffineMap n,0 ))) `| REAL ) . x = - ((1 / n) * (sin (n * x))) ; :: thesis: verum

end;

A11: dom (sin * (AffineMap n,0 )) = [#] REAL by FUNCT_2:def 1;
then A12: sin * (AffineMap n,0 ) is_differentiable_on REAL by A4, FDIFF_4:37;
A13: dom ((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) = REAL by FUNCT_2:def 1;
then A14: (AffineMap (1 / n),0 ) (#) (sin * (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 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))

proof

let x be Real; :: thesis: ( x in REAL implies (((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x))) )
assume x in REAL ; :: thesis: (((AffineMap (1 / n),0 ) (#) (sin * (AffineMap n,0 ))) `| REAL ) . x = ((1 / n) * (sin . (n * x))) + (x * (cos . (n * x)))
(((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 A13, A1, A3, A12, 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 A3, FDIFF_1:def 8
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (diff (sin * (AffineMap n,0 )),x)) by A1, A2, FDIFF_1:31
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (((sin * (AffineMap n,0 )) `| REAL ) . x)) by A12, FDIFF_1:def 8
.= (((sin * (AffineMap n,0 )) . x) * (1 / n)) + (((AffineMap (1 / n),0 ) . x) * (n * (cos . ((n * x) + 0 )))) by A11, A4, 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 A11, 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 A9, 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: verum

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

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