set f = cosec | [.(- (PI / 2)),0.[;
A1: (cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),0.[ =
rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),0.[)
by RELAT_1:115
.=
rng (cosec | [.(- (PI / 2)),0.[)
by RELAT_1:73
.=
cosec .: [.(- (PI / 2)),0.[
by RELAT_1:115
;
(cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),0.[ = cosec | [.(- (PI / 2)),0.[
by RELAT_1:73;
hence
arccosec1 | (cosec .: [.(- (PI / 2)),0.[) is decreasing
by A1, Th19, FCONT_3:10; verum