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;
( x in ].0,(PI / 2).[ implies diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
assume A3:
x in ].0,(PI / 2).[
;
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))
;
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; verum