let n be Element of NAT ; :: thesis: ( (- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos ) is_differentiable_on REAL & ( for x being Real holds (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = ((cos . x) #Z n) * (sin . x) ) )
A1: [#] REAL = dom ((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) by FUNCT_2:def 1;
for x0 being Real holds (#Z (n + 1)) * cos is_differentiable_in x0

proof

let x0 be Real; :: thesis: (#Z (n + 1)) * cos is_differentiable_in x0
cos is_differentiable_in x0 by SIN_COS:68;
hence (#Z (n + 1)) * cos is_differentiable_in x0 by TAYLOR_1:3; :: thesis: verum

end;

then A2: for x0 being Real st x0 in REAL holds
(#Z (n + 1)) * cos is_differentiable_in x0 ;
( [#] REAL = dom (#Z (n + 1)) & REAL = dom ((#Z (n + 1)) * cos ) ) by FUNCT_2:def 1;
then A3: (#Z (n + 1)) * cos is_differentiable_on REAL by A2, FDIFF_1:16;
A4: for x being Real st x in REAL holds
(((#Z (n + 1)) * cos ) `| REAL ) . x = ((- (n + 1)) * ((cos . x) #Z n)) * (sin . x)

proof

set m = n + 1;
let x be Real; :: thesis: ( x in REAL implies (((#Z (n + 1)) * cos ) `| REAL ) . x = ((- (n + 1)) * ((cos . x) #Z n)) * (sin . x) )
assume x in REAL ; :: thesis: (((#Z (n + 1)) * cos ) `| REAL ) . x = ((- (n + 1)) * ((cos . x) #Z n)) * (sin . x)
cos is_differentiable_in x by SIN_COS:68;
then diff ((#Z (n + 1)) * cos ),x = ((n + 1) * ((cos . x) #Z ((n + 1) - 1))) * (diff cos ,x) by TAYLOR_1:3
.= ((n + 1) * ((cos . x) #Z ((n + 1) - 1))) * (- (sin . x)) by SIN_COS:68
.= ((- (n + 1)) * ((cos . x) #Z ((n + 1) - 1))) * (sin . x) ;
hence (((#Z (n + 1)) * cos ) `| REAL ) . x = ((- (n + 1)) * ((cos . x) #Z n)) * (sin . x) by A3, FDIFF_1:def 8; :: thesis: verum

end;

for x being Real st x in REAL holds
(((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = ((cos . x) #Z n) * (sin . x)

proof

let x be Real; :: thesis: ( x in REAL implies (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = ((cos . x) #Z n) * (sin . x) )
assume x in REAL ; :: thesis: (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = ((cos . x) #Z n) * (sin . x)
(((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = (- (1 / (n + 1))) * (diff ((#Z (n + 1)) * cos ),x) by A1, A3, FDIFF_1:28
.= (- (1 / (n + 1))) * ((((#Z (n + 1)) * cos ) `| REAL ) . x) by A3, FDIFF_1:def 8
.= (- (1 / (n + 1))) * (((- (n + 1)) * ((cos . x) #Z n)) * (sin . x)) by A4
.= (((1 / (n + 1)) * (n + 1)) * ((cos . x) #Z n)) * (sin . x)
.= (((n + 1) / (n + 1)) * ((cos . x) #Z n)) * (sin . x) by XCMPLX_1:100
.= (1 * ((cos . x) #Z n)) * (sin . x) by XCMPLX_1:60 ;
hence (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = ((cos . x) #Z n) * (sin . x) ; :: thesis: verum

end;

hence ( (- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos ) is_differentiable_on REAL & ( for x being Real holds (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos )) `| REAL ) . x = ((cos . x) #Z n) * (sin . x) ) ) by A1, A3, FDIFF_1:28; :: thesis: verum