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, XBOOLE_1:1;
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 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 ].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