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:47, RELAT_1:72;
then
(arcsec2 | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is continuous
by Th42, Th50, RELAT_1:115;
hence
arcsec2 | [.(- (sqrt 2)),(- 1).] is continuous
by FCONT_1:15; verum