set f = cosec | [.(- (PI / 2)),(- (PI / 4)).];
A1: (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] = cosec | [.(- (PI / 2)),(- (PI / 4)).] by RELAT_1:101;
- (PI / 2) <= - (PI / 4) by Lm11, XXREAL_1:3;
then (((cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).]) " ) | ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) .: [.(- (PI / 2)),(- (PI / 4)).]) is continuous by Lm15, Lm23, FCONT_1:54;
then (arccosec1 | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is continuous by A1, Th43, Th51, RELAT_1:148;
hence arccosec1 | [.(- (sqrt 2)),(- 1).] is continuous by FCONT_1:16; :: thesis: verum