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