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; :: thesis: verum