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:28, A;
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:21;
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:70;
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:16;
((- (cot * exp_R )) `| Z) . x = diff (- (cot * exp_R )),x by A4, A6, FDIFF_1:def 8
.= (- 1) * (diff (cot * exp_R ),x) by A10, FDIFF_1:23, A
.= (- 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:70 ;
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