A1: 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:
assume A2: th in dom (tan | [.0 ,1.]) ; :: thesis:
A3: th in [.0 ,1.] by A2, RELAT_1:86;
A4: dom sin = REAL by FUNCT_2:def 1;
A5: th in dom sin by A4, XREAL_0:def 1;
A6: th in [#] REAL by XREAL_0:def 1;
A7: sin is_differentiable_in th by A6, Th73, FDIFF_1:16;
A8: sin is_continuous_in th by A7, FDIFF_1:32;
A9: cos is_differentiable_in th by A6, Th72, FDIFF_1:16;
A10: cos is_continuous_in th by A9, FDIFF_1:32;
A11: cos . th <> 0 by A3, Th74;
A12: tan is_continuous_in th by A5, A8, A10, A11, FCONT_1:11;

A13: now

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

A18: now

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

end;

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

end;

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

end;

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