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

proof

let th be real number ; :: thesis: ( th in dom (sec | [.0 ,(PI / 2).[) implies sec | [.0 ,(PI / 2).[ is_continuous_in th )
assume th in dom (sec | [.0 ,(PI / 2).[) ; :: thesis: sec | [.0 ,(PI / 2).[ is_continuous_in th
then A0: th in [.0 ,(PI / 2).[ by RELAT_1:86;
A1: cos . th <> 0 by A0, Lm1, COMPTRIG:27;
AA: cos is_differentiable_in th by SIN_COS:68;
A2: sec is_continuous_in th by A1, AA, FCONT_1:10, FDIFF_1:32;
( th in dom (sec | [.0 ,(PI / 2).[) & ( for rseq being Real_Sequence st rng rseq c= dom (sec | [.0 ,(PI / 2).[) & rseq is convergent & lim rseq = th holds
( (sec | [.0 ,(PI / 2).[) /* rseq is convergent & (sec | [.0 ,(PI / 2).[) . th = lim ((sec | [.0 ,(PI / 2).[) /* rseq) ) ) )

proof

now

let rseq be Real_Sequence; :: thesis: ( rng rseq c= dom (sec | [.0 ,(PI / 2).[) & rseq is convergent & lim rseq = th implies ( (sec | [.0 ,(PI / 2).[) /* rseq is convergent & (sec | [.0 ,(PI / 2).[) . th = lim ((sec | [.0 ,(PI / 2).[) /* rseq) ) )
assume A3: ( rng rseq c= dom (sec | [.0 ,(PI / 2).[) & rseq is convergent & lim rseq = th ) ; :: thesis: ( (sec | [.0 ,(PI / 2).[) /* rseq is convergent & (sec | [.0 ,(PI / 2).[) . th = lim ((sec | [.0 ,(PI / 2).[) /* rseq) )
A4: dom (sec | [.0 ,(PI / 2).[) = [.0 ,(PI / 2).[ by Th1, RELAT_1:91;
then rng rseq c= dom sec by A3, Th1, XBOOLE_1:1;
then A6: ( sec /* rseq is convergent & sec . th = lim (sec /* rseq) ) by A2, A3, FCONT_1:def 1;
(sec | [.0 ,(PI / 2).[) /* rseq = sec /* rseq

proof

now

let n be Element of NAT ; :: thesis: ((sec | [.0 ,(PI / 2).[) /* 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 | [.0 ,(PI / 2).[) . (rseq . n) = sec . (rseq . n) by A3, A4, FUNCT_1:72;
(sec | [.0 ,(PI / 2).[) . (rseq . n) = ((sec | [.0 ,(PI / 2).[) /* rseq) . n by A3, FUNCT_2:185;
hence ((sec | [.0 ,(PI / 2).[) /* rseq) . n = (sec /* rseq) . n by A3, A4, A7, Th1, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence (sec | [.0 ,(PI / 2).[) /* rseq = sec /* rseq by FUNCT_2:113; :: thesis: verum

end;

hence ( (sec | [.0 ,(PI / 2).[) /* rseq is convergent & (sec | [.0 ,(PI / 2).[) . th = lim ((sec | [.0 ,(PI / 2).[) /* rseq) ) by A0, A6, Lm17; :: thesis: verum

end;

hence ( th in dom (sec | [.0 ,(PI / 2).[) & ( for rseq being Real_Sequence st rng rseq c= dom (sec | [.0 ,(PI / 2).[) & rseq is convergent & lim rseq = th holds
( (sec | [.0 ,(PI / 2).[) /* rseq is convergent & (sec | [.0 ,(PI / 2).[) . th = lim ((sec | [.0 ,(PI / 2).[) /* rseq) ) ) ) by A0, Lm17; :: thesis: verum

end;

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

end;

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