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;
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 7
.= - ((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