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; :: thesis: verum