for th being real number st th in dom (tan | [.0 ,1.]) holds
tan | [.0 ,1.] is_continuous_in th

proof

let th be real number ; :: thesis: ( th in dom (tan | [.0 ,1.]) implies tan | [.0 ,1.] is_continuous_in th )
assume A2: th in dom (tan | [.0 ,1.]) ; :: thesis: tan | [.0 ,1.] is_continuous_in th
then A3: th in [.0 ,1.] by RELAT_1:86;
dom sin = REAL by FUNCT_2:def 1;
then A5: th in dom sin by XREAL_0:def 1;
A6: th in [#] REAL by XREAL_0:def 1;
then sin is_differentiable_in th by Th73, FDIFF_1:16;
then A8: sin is_continuous_in th by FDIFF_1:32;
cos is_differentiable_in th by A6, Th72, FDIFF_1:16;
then A10: cos is_continuous_in th by FDIFF_1:32;
cos . th <> 0 by A3, Th74;
then A12: tan is_continuous_in th by A5, A8, A10, FCONT_1:11;

now

let rseq be Real_Sequence; :: thesis: ( rng rseq c= dom (tan | [.0 ,1.]) & rseq is convergent & lim rseq = th implies ( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) ) )
assume that
A14: rng rseq c= dom (tan | [.0 ,1.]) and
A15: ( rseq is convergent & lim rseq = th ) ; :: thesis: ( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) )
A16: rng rseq c= dom tan by A14, Lm15, Th75, XBOOLE_1:1;
then A17: tan . th = lim (tan /* rseq) by A12, A15, FCONT_1:def 1;

now

let k1 be Element of NAT ; :: thesis: ((tan | [.0 ,1.]) /* rseq) . k1 = (tan /* rseq) . k1
dom rseq = NAT by SEQ_1:3;
then rseq . k1 in rng rseq by FUNCT_1:def 5;
then A21: (tan | [.0 ,1.]) . (rseq . k1) = tan . (rseq . k1) by A14, Lm15;
(tan | [.0 ,1.]) . (rseq . k1) = ((tan | [.0 ,1.]) /* rseq) . k1 by A14, FUNCT_2:185;
hence ((tan | [.0 ,1.]) /* rseq) . k1 = (tan /* rseq) . k1 by A14, A21, Lm15, Th75, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

then (tan | [.0 ,1.]) /* rseq = tan /* rseq by FUNCT_2:113;
hence ( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) ) by A2, A12, A15, A16, A17, Lm15, FCONT_1:def 1; :: thesis: verum

end;

hence tan | [.0 ,1.] is_continuous_in th by FCONT_1:def 1; :: thesis: verum

end;

hence tan | [.0 ,1.] is continuous by FCONT_1:def 2; :: thesis: verum