set f = cosec | [.(PI / 4),(PI / 2).];
PI / 4 <= PI / 2 by Lm8, XXREAL_1:2;
then ( (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] = cosec | [.(PI / 4),(PI / 2).] & (((cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).]) ") | ((cosec | [.(PI / 4),(PI / 2).]) .: [.(PI / 4),(PI / 2).]) is continuous ) by Lm32, Lm40, FCONT_1:47, RELAT_1:72;
then (arccosec2 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous by Th44, Th52, RELAT_1:115;
hence arccosec2 | [.1,(sqrt 2).] is continuous by FCONT_1:15; :: thesis: verum