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 B1: th in dom (tan | [.0 ,1.]) ; :: thesis: tan | [.0 ,1.] is_continuous_in th
then A1: th in [.0 ,1.] by RELAT_1:86;
dom sin = REAL by FUNCT_2:def 1;
then X: th in dom sin by XREAL_0:def 1;
A2: th in [#] REAL by XREAL_0:def 1;
then sin is_differentiable_in th by Th73, FDIFF_1:16;
then A3: sin is_continuous_in th by FDIFF_1:32;
cos is_differentiable_in th by A2, Th72, FDIFF_1:16;
then A4: cos is_continuous_in th by FDIFF_1:32;
cos . th <> 0 by A1, Th74;
then A5: tan is_continuous_in th by A3, A4, X, FCONT_1:11;
( th in dom (tan | [.0 ,1.]) & ( for rseq being Real_Sequence st rng rseq c= dom (tan | [.0 ,1.]) & rseq is convergent & lim rseq = th holds
( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) ) ) )

proof

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 A6: ( rng rseq c= dom (tan | [.0 ,1.]) & rseq is convergent & lim rseq = th ) ; :: thesis: ( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) )
then rng rseq c= dom tan by Lm19, Th75, XBOOLE_1:1;
then A8: ( tan /* rseq is convergent & tan . th = lim (tan /* rseq) ) by A5, A6, FCONT_1:def 1;
(tan | [.0 ,1.]) /* rseq = tan /* rseq

proof

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 A9: (tan | [.0 ,1.]) . (rseq . k1) = tan . (rseq . k1) by A6, Lm19;
(tan | [.0 ,1.]) . (rseq . k1) = ((tan | [.0 ,1.]) /* rseq) . k1 by A6, FUNCT_2:185;
hence ((tan | [.0 ,1.]) /* rseq) . k1 = (tan /* rseq) . k1 by A6, A9, Lm19, Th75, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

hence (tan | [.0 ,1.]) /* rseq = tan /* rseq by FUNCT_2:113; :: thesis: verum

end;

hence ( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) ) by B1, A8, Lm19; :: thesis: verum

end;

hence ( th in dom (tan | [.0 ,1.]) & ( for rseq being Real_Sequence st rng rseq c= dom (tan | [.0 ,1.]) & rseq is convergent & lim rseq = th holds
( (tan | [.0 ,1.]) /* rseq is convergent & (tan | [.0 ,1.]) . th = lim ((tan | [.0 ,1.]) /* rseq) ) ) ) by B1; :: 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