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