let Z be open Subset of REAL; :: thesis: ( Z c= dom (ln * cosec) implies ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * cosec)) `| Z) . x = cot . x ) ) )
assume A1: Z c= dom (ln * cosec) ; :: thesis: ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * cosec)) `| Z) . x = cot . x ) )
then A2: Z c= dom (- (ln * cosec)) by VALUED_1:8;
A3: ln * cosec is_differentiable_on Z by A1, FDIFF_9:19;
then A4: (- 1) (#) (ln * cosec) is_differentiable_on Z by A2, FDIFF_1:20;
A5: 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 cosec by A1, FUNCT_1:11;
hence sin . x <> 0 by RFUNCT_1:3; :: thesis: verum

end;

for x being Real st x in Z holds
((- (ln * cosec)) `| Z) . x = cot . x

proof

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

end;

hence ( - (ln * cosec) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (ln * cosec)) `| Z) . x = cot . x ) ) by A4; :: thesis: verum