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

proof

let x be Real; :: thesis: ( x in ].0,(PI / 2).[ implies diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
assume A3: x in ].0,(PI / 2).[ ; :: thesis: diff (cosec,x) = - ((cos . x) / ((sin . x) ^2))
then diff (cosec,x) = (cosec `| ].0,(PI / 2).[) . 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 ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds
diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) by A1, FDIFF_9:5; :: thesis: verum