theorem Th4: :: INTEGR11:4

for n being Element of NAT holds
( (- (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) ) )