for th being real number st th in dom (sec | ].(PI / 2),PI .]) holds
sec | ].(PI / 2),PI .] is_continuous_in th

proof

let th be real number ; :: thesis: ( th in dom (sec | ].(PI / 2),PI .]) implies sec | ].(PI / 2),PI .] is_continuous_in th )
A1: cos is_differentiable_in th by SIN_COS:68;
assume A2: th in dom (sec | ].(PI / 2),PI .]) ; :: thesis: sec | ].(PI / 2),PI .] is_continuous_in th
then th in ].(PI / 2),PI .] by RELAT_1:86;
then cos . th <> 0 by Lm2, COMPTRIG:29;
then A3: sec is_continuous_in th by A1, FCONT_1:10, FDIFF_1:32;

now

let rseq be Real_Sequence; :: thesis: ( rng rseq c= dom (sec | ].(PI / 2),PI .]) & rseq is convergent & lim rseq = th implies ( (sec | ].(PI / 2),PI .]) /* rseq is convergent & (sec | ].(PI / 2),PI .]) . th = lim ((sec | ].(PI / 2),PI .]) /* rseq) ) )
assume that
A4: rng rseq c= dom (sec | ].(PI / 2),PI .]) and
A5: ( rseq is convergent & lim rseq = th ) ; :: thesis: ( (sec | ].(PI / 2),PI .]) /* rseq is convergent & (sec | ].(PI / 2),PI .]) . th = lim ((sec | ].(PI / 2),PI .]) /* rseq) )
A6: dom (sec | ].(PI / 2),PI .]) = ].(PI / 2),PI .] by Th2, RELAT_1:91;

now

let n be Element of NAT ; :: thesis: ((sec | ].(PI / 2),PI .]) /* rseq) . n = (sec /* rseq) . n
dom rseq = NAT by SEQ_1:3;
then rseq . n in rng rseq by FUNCT_1:def 5;
then A7: (sec | ].(PI / 2),PI .]) . (rseq . n) = sec . (rseq . n) by A4, A6, FUNCT_1:72;
(sec | ].(PI / 2),PI .]) . (rseq . n) = ((sec | ].(PI / 2),PI .]) /* rseq) . n by A4, FUNCT_2:185;
hence ((sec | ].(PI / 2),PI .]) /* rseq) . n = (sec /* rseq) . n by A4, A6, A7, Th2, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then A8: (sec | ].(PI / 2),PI .]) /* rseq = sec /* rseq by FUNCT_2:113;
A9: rng rseq c= dom sec by A4, A6, Th2, XBOOLE_1:1;
then sec . th = lim (sec /* rseq) by A3, A5, FCONT_1:def 1;
hence ( (sec | ].(PI / 2),PI .]) /* rseq is convergent & (sec | ].(PI / 2),PI .]) . th = lim ((sec | ].(PI / 2),PI .]) /* rseq) ) by A2, A3, A5, A9, A8, Lm34, FCONT_1:def 1; :: thesis: verum

end;

hence sec | ].(PI / 2),PI .] is_continuous_in th by FCONT_1:def 1; :: thesis: verum

end;

hence sec | ].(PI / 2),PI .] is continuous by FCONT_1:def 2; :: thesis: verum