set f = sec | [.0 ,(PI / 4).];
A1: (sec | [.0 ,(PI / 4).]) | [.0 ,(PI / 4).] = sec | [.0 ,(PI / 4).] by RELAT_1:101;
(((sec | [.0 ,(PI / 4).]) | [.0 ,(PI / 4).]) " ) | ((sec | [.0 ,(PI / 4).]) .: [.0 ,(PI / 4).]) is continuous by Lm13, Lm21, FCONT_1:54;
then (arcsec1 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous by A1, Th41, Th49, RELAT_1:148;
hence arcsec1 | [.1,(sqrt 2).] is continuous by FCONT_1:16; :: thesis: verum