set Z = ].(- (PI / 2)),0 .[;
[.(- (PI / 2)),0 .[ = ].(- (PI / 2)),0 .[ \/ {(- (PI / 2))} by XXREAL_1:131;
then ].(- (PI / 2)),0 .[ c= [.(- (PI / 2)),0 .[ by XBOOLE_1:7;
then A1: ].(- (PI / 2)),0 .[ c= dom cosec by Th3, XBOOLE_1:1;
then A2: cosec is_differentiable_on ].(- (PI / 2)),0 .[ by FDIFF_9:5;
for x being Real st x in ].(- (PI / 2)),0 .[ holds
diff cosec ,x = - ((cos . x) / ((sin . x) ^2 ))

proof

let x be Real; :: thesis: ( x in ].(- (PI / 2)),0 .[ implies diff cosec ,x = - ((cos . x) / ((sin . x) ^2 )) )
assume A3: x in ].(- (PI / 2)),0 .[ ; :: thesis: diff cosec ,x = - ((cos . x) / ((sin . x) ^2 ))
then diff cosec ,x = (cosec `| ].(- (PI / 2)),0 .[) . x by A2, FDIFF_1:def 8
.= - ((cos . x) / ((sin . x) ^2 )) by A1, A3, FDIFF_9:5 ;
hence diff cosec ,x = - ((cos . x) / ((sin . x) ^2 )) ; :: thesis: verum

end;

hence ( cosec is_differentiable_on ].(- (PI / 2)),0 .[ & ( for x being Real st x in ].(- (PI / 2)),0 .[ holds
diff cosec ,x = - ((cos . x) / ((sin . x) ^2 )) ) ) by A1, FDIFF_9:5; :: thesis: verum