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:63;
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:9;
hence (- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos) is_differentiable_on REAL by A1, FDIFF_1:20; :: thesis: for x being Real holds (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) . x = ((cos . x) #Z n) * (sin . x)
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 A5: 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:63;
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:63
.= ((- (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 7, A5; :: thesis: verum

end;

A6: 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 A7: 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:20, A7
.= (- (1 / (n + 1))) * ((((#Z (n + 1)) * cos) `| REAL) . x) by A3, FDIFF_1:def 7, A7
.= (- (1 / (n + 1))) * (((- (n + 1)) * ((cos . x) #Z n)) * (sin . x)) by A4, A7
.= (((1 / (n + 1)) * (n + 1)) * ((cos . x) #Z n)) * (sin . x)
.= (((n + 1) / (n + 1)) * ((cos . x) #Z n)) * (sin . x) by XCMPLX_1:99
.= (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;

let x be Real; :: thesis: (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) . x = ((cos . x) #Z n) * (sin . x)
x in REAL by XREAL_0:def 1;
hence (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) . x = ((cos . x) #Z n) * (sin . x) by A6; :: thesis: verum