set f = sec | [.0,(PI / 4).];
( (sec | [.0,(PI / 4).]) | [.0,(PI / 4).] = sec | [.0,(PI / 4).] & (((sec | [.0,(PI / 4).]) | [.0,(PI / 4).]) ") | ((sec | [.0,(PI / 4).]) .: [.0,(PI / 4).]) is continuous )
by Lm29, Lm37, FCONT_1:47, RELAT_1:72;
then
(arcsec1 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous
by Th41, Th49, RELAT_1:115;
hence
arcsec1 | [.1,(sqrt 2).] is continuous
by FCONT_1:15; verum