set f = sec | [.((3 / 4) * PI ),PI .];
A1: (sec | [.((3 / 4) * PI ),PI .]) | [.((3 / 4) * PI ),PI .] = sec | [.((3 / 4) * PI ),PI .] by RELAT_1:101;
(3 / 4) * PI <= PI by Lm10, XXREAL_1:2;
then (((sec | [.((3 / 4) * PI ),PI .]) | [.((3 / 4) * PI ),PI .]) " ) | ((sec | [.((3 / 4) * PI ),PI .]) .: [.((3 / 4) * PI ),PI .]) is continuous by Lm14, Lm22, FCONT_1:54;
then (arcsec2 | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is continuous by A1, Th42, Th50, RELAT_1:148;
hence arcsec2 | [.(- (sqrt 2)),(- 1).] is continuous by FCONT_1:16; :: thesis: verum