let n be Nat; :: thesis: for Z being open Subset of REAL st Z c= dom ((#Z n) * cosec) & 1 <= n holds
( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) )
let Z be open Subset of REAL; :: thesis: ( Z c= dom ((#Z n) * cosec) & 1 <= n implies ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) )
assume A1: ( Z c= dom ((#Z n) * cosec) & 1 <= n ) ; :: thesis: ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) )
then A2: ( Z c= dom (- ((#Z n) * cosec)) & 1 <= n ) by VALUED_1:8;
A3: (#Z n) * cosec is_differentiable_on Z by A1, FDIFF_9:21;
then A4: (- 1) (#) ((#Z n) * cosec) is_differentiable_on Z by A2, FDIFF_1:20;
for x being Real st x in Z holds
((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1))

proof

let x be Real; :: thesis: ( x in Z implies ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) )
assume A5: x in Z ; :: thesis: ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1))
((- ((#Z n) * cosec)) `| Z) . x = ((- 1) (#) (((#Z n) * cosec) `| Z)) . x by A3, FDIFF_2:19
.= (- 1) * ((((#Z n) * cosec) `| Z) . x) by VALUED_1:6
.= (- 1) * (- ((n * (cos . x)) / ((sin . x) #Z (n + 1)))) by A1, A5, FDIFF_9:21
.= (n * (cos . x)) / ((sin . x) #Z (n + 1)) ;
hence ((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ; :: thesis: verum

end;

hence ( - ((#Z n) * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * cosec)) `| Z) . x = (n * (cos . x)) / ((sin . x) #Z (n + 1)) ) ) by A4; :: thesis: verum