let Z be open Subset of REAL; :: thesis: ( Z c= dom (cot * exp_R) implies ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) ) )
assume A1: Z c= dom (cot * exp_R) ; :: thesis: ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) )
then A2: Z c= dom (- (cot * exp_R)) by VALUED_1:8;
A3: cot * exp_R is_differentiable_on Z by A1, FDIFF_8:13;
then A4: (- 1) (#) (cot * exp_R) is_differentiable_on Z by A2, FDIFF_1:20;
A5: for x being Real st x in Z holds
sin . (exp_R . x) <> 0

proof

let x be Real; :: thesis: ( x in Z implies sin . (exp_R . x) <> 0 )
assume x in Z ; :: thesis: sin . (exp_R . x) <> 0
then exp_R . x in dom (cos / sin) by A1, FUNCT_1:11;
hence sin . (exp_R . x) <> 0 by FDIFF_8:2; :: thesis: verum

end;

for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2)

proof

let x be Real; :: thesis: ( x in Z implies ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) )
assume A6: x in Z ; :: thesis: ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2)
A7: exp_R is_differentiable_in x by SIN_COS:65;
A8: sin . (exp_R . x) <> 0 by A5, A6;
then A9: cot is_differentiable_in exp_R . x by FDIFF_7:47;
A10: cot * exp_R is_differentiable_in x by A3, A6, FDIFF_1:9;
((- (cot * exp_R)) `| Z) . x = diff ((- (cot * exp_R)),x) by A4, A6, FDIFF_1:def 7
.= (- 1) * (diff ((cot * exp_R),x)) by A10, FDIFF_1:15
.= (- 1) * ((diff (cot,(exp_R . x))) * (diff (exp_R,x))) by A7, A9, FDIFF_2:13
.= (- 1) * ((- (1 / ((sin . (exp_R . x)) ^2))) * (diff (exp_R,x))) by A8, FDIFF_7:47
.= (- 1) * (- ((diff (exp_R,x)) / ((sin . (exp_R . x)) ^2)))
.= (exp_R . x) / ((sin . (exp_R . x)) ^2) by SIN_COS:65 ;
hence ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ; :: thesis: verum

end;

hence ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) ) by A4; :: thesis: verum