set f = cosec | ].0,(PI / 2).];
A1: (cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).] =
rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).])
by RELAT_1:115
.=
rng (cosec | ].0,(PI / 2).])
by RELAT_1:73
.=
cosec .: ].0,(PI / 2).]
by RELAT_1:115
;
(cosec | ].0,(PI / 2).]) | ].0,(PI / 2).] = cosec | ].0,(PI / 2).]
by RELAT_1:73;
hence
arccosec2 | (cosec .: ].0,(PI / 2).]) is decreasing
by A1, Th20, FCONT_3:10; verum