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

proof

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

end;

A3: exp_R * cot is_differentiable_on Z by A1, FDIFF_8:17;
then A4: (- 1) (#) (exp_R * cot ) is_differentiable_on Z by A2, FDIFF_1:28, A;
for x being Real st x in Z holds
((- (exp_R * cot )) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2 )

proof

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

end;

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