set f = cosec | [.(PI / 4),(PI / 2).];
A1: (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] = cosec | [.(PI / 4),(PI / 2).] by RELAT_1:101;
PI / 4 <= PI / 2 by Lm12, XXREAL_1:2;
then (((cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).]) " ) | ((cosec | [.(PI / 4),(PI / 2).]) .: [.(PI / 4),(PI / 2).]) is continuous by Lm16, Lm24, FCONT_1:54;
then (arccosec2 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous by A1, Th44, Th52, RELAT_1:148;
hence arccosec2 | [.1,(sqrt 2).] is continuous by FCONT_1:16; :: thesis: verum