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:54, RELAT_1:101;
then (arcsec1 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous by Th41, Th49, RELAT_1:148;
hence arcsec1 | [.1,(sqrt 2).] is continuous by FCONT_1:16; :: thesis: verum